1  /-
  2  Copyright (c) 2017 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
  5  -/
  6  
  7  import topology.continuous_on
src         └────────────────────┘
  8  
  9  /-!
 10  # Properties of subsets of topological spaces
 11  
 12  ## Main definitions
 13  
 14  `compact`, `is_clopen`, `is_irreducible`, `is_connected`, `is_totally_disconnected`, `is_totally_separated`
 15  
 16  TODO: write better docs
 17  -/
 18  
 19  open set filter lattice classical
 20  open_locale classical topological_space
 21  
 22  universes u v
 23  variables {α : Type u} {β : Type v} [topological_space α]
id                                       └───────────────┘
src                                       └───────────────┘
typ                                      └───────────────┘
doc                                       └───────────────┘
 24  
 25  /- compact sets -/
 26  section compact
 27  
 28  /-- A set `s` is compact if for every filter `f` that contains `s`,
 29      every set of `f` also meets every neighborhood of some `a ∈ s`. -/
 30  def compact (s : set α) := ∀f, f ≠ ⊥ → f ≤ principal s → ∃a∈s, f ⊓ 𝓝 a ≠ ⊥
id                    └─┘                └───────┘           
src                   └─┘                    └───────┘                
typ                   └─┘                └───────┘           
doc                                             └───────┘               
 31  
 32  lemma compact.inter_right {s t : set α} (hs : compact s) (ht : is_closed t) : compact (s ∩ t) :=
id                                    └─┘         └─────┘         └───────┘     └─────┘    
src                                   └─┘          └─────┘          └───────┘      └─────┘    
typ                                   └─┘         └─────┘         └───────┘     └─────┘    
doc                                                └─────┘          └───────┘      └─────┘
 33  assume f hnf hstf,
id           └─┘ └──┘
typ          └─┘ └──┘
 34  let ⟨a, hsa, (ha : f ⊓ 𝓝 a ≠ ⊥)⟩ := hs f hnf (le_trans hstf (le_principal_iff.2 (inter_subset_left _ _))) in
id   └─┘    └─┘                   └┘  └─┘  └──────┘ └──┘  └──────────────┘   └───────────────┘
src                                            └──────┘       └──────────────┘   └───────────────┘
typ  └─┘    └─┘                   └┘  └─┘  └──────┘ └──┘  └──────────────┘   └───────────────┘
doc                         
 35  have a ∈ t,
id           
src         
typ          
 36    from ht.mem_of_nhds_within_ne_bot $ ne_bot_of_le_ne_bot (by { rw inf_comm at ha, exact ha }) $
id          └┘└────────────────────────┘   └─────────────────┘          └──────┘              └┘
src           └────────────────────────┘   └─────────────────┘       └─┘└──────┘└────┘  └────┘  
typ         └┘└────────────────────────┘   └─────────────────┘       └─┘└──────┘└────┘  └────┘└┘
doc                                                                  └─┘        └────┘  └────┘  
txt                                                                  └─┘        └────┘  └────┘  
par                                                                  └─┘        └────┘  └────┘  
pid                                                                            └────┘         
st                                                                └──────────────────┘└─────────┘└┘
 37      inf_le_inf (le_refl _) (le_trans hstf (le_principal_iff.2 (inter_subset_right _ _))),
id       └────────┘  └─────┘     └──────┘ └──┘  └──────────────┘   └────────────────┘
src      └────────┘  └─────┘     └──────┘       └──────────────┘   └────────────────┘
typ      └────────┘  └─────┘     └──────┘ └──┘  └──────────────┘   └────────────────┘
 38  ⟨a, ⟨hsa, this⟩, ha⟩
id             └──┘
typ            └──┘
 39  
 40  lemma compact.inter_left {s t : set α} (ht : compact t) (hs : is_closed s) : compact (s ∩ t) :=
id                                   └─┘         └─────┘         └───────┘     └─────┘    
src                                  └─┘          └─────┘          └───────┘      └─────┘    
typ                                  └─┘         └─────┘         └───────┘     └─────┘    
doc                                               └─────┘          └───────┘      └─────┘
 41  inter_comm t s ▸ ht.inter_right hs
id   └────────┘    └┘└──────────┘ └┘
src  └────────┘        └──────────┘
typ  └────────┘    └┘└──────────┘ └┘
 42  
 43  lemma compact_diff {s t : set α} (hs : compact s) (ht : is_open t) : compact (s \ t) :=
id                             └─┘         └─────┘         └─────┘     └─────┘    
src                            └─┘          └─────┘          └─────┘      └─────┘    
typ                            └─┘         └─────┘         └─────┘     └─────┘    
doc                                         └─────┘          └─────┘      └─────┘
 44  hs.inter_right (is_closed_compl_iff.mpr ht)
id   └┘└──────────┘  └─────────────────┘└──┘ └┘
src    └──────────┘  └─────────────────┘└──┘
typ  └┘└──────────┘  └─────────────────┘└──┘ └┘
 45  
 46  lemma compact_of_is_closed_subset {s t : set α}
id                                            └─┘ 
src                                           └─┘
typ                                           └─┘ 
 47    (hs : compact s) (ht : is_closed t) (h : t ⊆ s) : compact t :=
id           └─────┘         └───────┘              └─────┘ 
src          └─────┘          └───────┘                 └─────┘
typ          └─────┘         └───────┘              └─────┘ 
doc          └─────┘          └───────┘                  └─────┘
 48  inter_eq_self_of_subset_right h ▸ hs.inter_right ht
id   └───────────────────────────┘   └┘└──────────┘ └┘
src  └───────────────────────────┘      └──────────┘
typ  └───────────────────────────┘   └┘└──────────┘ └┘
 49  
 50  lemma compact.adherence_nhdset {s t : set α} {f : filter α}
id                                         └─┘        └────┘ 
src                                        └─┘         └────┘
typ                                        └─┘        └────┘ 
 51    (hs : compact s) (hf₂ : f ≤ principal s) (ht₁ : is_open t) (ht₂ : ∀a∈s, 𝓝 a ⊓ f ≠ ⊥ → a ∈ t) :
id           └─────┘            └───────┘          └─────┘                        
src          └─────┘              └───────┘           └─────┘                            
typ          └─────┘            └───────┘          └─────┘                        
doc          └─────┘               └───────┘           └─────┘                 
 52    t ∈ f :=
id       
src      
typ      
 53  classical.by_cases mem_sets_of_eq_bot $
id   └────────────────┘ └────────────────┘
src  └────────────────┘ └────────────────┘
typ  └────────────────┘ └────────────────┘
 54    assume : f ⊓ principal (- t) ≠ ⊥,
id                └───────┘      
src                └───────┘       
typ               └───────┘      
doc                 └───────┘
 55    let ⟨a, ha, (hfa : f ⊓ principal (-t) ⊓ 𝓝 a ≠ ⊥)⟩ := hs _ this $ inf_le_left_of_le hf₂ in
id     └─┘    └┘          └───────┘               └┘   └──┘   └───────────────┘ └─┘
src                          └───────┘                            └───────────────┘
typ    └─┘    └┘          └───────┘               └┘   └──┘   └───────────────┘ └─┘
doc                           └───────┘        
 56    have a ∈ t,
id             
src           
typ            
 57      from ht₂ a ha $ ne_bot_of_le_ne_bot hfa $ le_inf inf_le_right $ inf_le_left_of_le inf_le_left,
id            └─┘        └─────────────────┘       └────┘ └──────────┘   └───────────────┘ └─────────┘
src                      └─────────────────┘       └────┘ └──────────┘   └───────────────┘ └─────────┘
typ           └─┘        └─────────────────┘       └────┘ └──────────┘   └───────────────┘ └─────────┘
 58    have (-t) ∩ t ∈ nhds_within a (-t),
id                └─────────┘    
src                 └─────────┘    
typ               └─────────┘    
doc                    └─────────┘
 59      from inter_mem_nhds_within _ (mem_nhds_sets ht₁ this),
id            └───────────────────┘    └───────────┘ └─┘ └──┘
src           └───────────────────┘    └───────────┘
typ           └───────────────────┘    └───────────┘ └─┘ └──┘
 60    have A : nhds_within a (-t) = ⊥,
id              └─────────┘       
src             └─────────┘        
typ             └─────────┘       
doc             └─────────┘
 61      from empty_in_sets_eq_bot.1 $ compl_inter_self t ▸ this,
id            └──────────────────┘    └──────────────┘   └──┘
src           └──────────────────┘    └──────────────┘   
typ           └──────────────────┘    └──────────────┘   └──┘
 62    have nhds_within a (-t) ≠ ⊥,
id          └─────────┘       
src         └─────────┘        
typ         └─────────┘       
doc         └─────────┘
 63      from ne_bot_of_le_ne_bot hfa $ le_inf inf_le_right $ inf_le_left_of_le inf_le_right,
id            └─────────────────┘       └────┘ └──────────┘   └───────────────┘ └──────────┘
src           └─────────────────┘       └────┘ └──────────┘   └───────────────┘ └──────────┘
typ           └─────────────────┘       └────┘ └──────────┘   └───────────────┘ └──────────┘
 64    absurd A this
id     └────┘  └──┘
src    └────┘
typ    └────┘  └──┘
 65  
 66  lemma compact_iff_ultrafilter_le_nhds {s : set α} :
id                                              └─┘ 
src                                             └─┘
typ                                             └─┘ 
 67    compact s ↔ (∀f, is_ultrafilter f → f ≤ principal s → ∃a∈s, f ≤ 𝓝 a) :=
id     └─────┘       └────────────┘      └───────┘         
src    └─────┘         └────────────┘        └───────┘            
typ    └─────┘       └────────────┘      └───────┘         
doc    └─────┘          └────────────┘         └───────┘               
 68  ⟨assume hs : compact s, assume f hf hfs,
id                └─────┘           └┘ └─┘
src               └─────┘
typ               └─────┘           └┘ └─┘
doc               └─────┘
 69    let ⟨a, ha, h⟩ := hs _ hf.left hfs in
id     └─┘    └┘       └┘   └┘└───┘ └─┘
src                             └───┘
typ    └─┘    └┘       └┘   └┘└───┘ └─┘
 70    ⟨a, ha, le_of_ultrafilter hf h⟩,
id             └───────────────┘ └┘
src            └───────────────┘
typ            └───────────────┘ └┘
 71  
 72    assume hs : (∀f, is_ultrafilter f → f ≤ principal s → ∃a∈s, f ≤ 𝓝 a),
id                     └────────────┘      └───────┘         
src                     └────────────┘        └───────┘            
typ                    └────────────┘      └───────┘         
doc                     └────────────┘         └───────┘               
 73    assume f hf hfs,
id             └┘ └─┘
typ            └┘ └─┘
 74    let ⟨a, ha, (h : ultrafilter_of f ≤ 𝓝 a)⟩ :=
id     └─┘    └┘       └────────────┘   
src                     └────────────┘    
typ    └─┘    └┘       └────────────┘   
doc                     └────────────┘     
 75      hs (ultrafilter_of f) (ultrafilter_ultrafilter_of hf) (le_trans ultrafilter_of_le hfs) in
id       └┘  └────────────┘    └────────────────────────┘ └┘   └──────┘ └───────────────┘ └─┘
src          └────────────┘     └────────────────────────┘      └──────┘ └───────────────┘
typ      └┘  └────────────┘    └────────────────────────┘ └┘   └──────┘ └───────────────┘ └─┘
doc          └────────────┘
 76    have ultrafilter_of f ⊓ 𝓝 a ≠ ⊥,
id          └────────────┘       
src         └────────────┘        
typ         └────────────┘       
doc         └────────────┘     
 77      by simp only [inf_of_le_left, h]; exact (ultrafilter_ultrafilter_of hf).left,
id                     └────────────┘            └────────────────────────┘ └┘
src         └─────────┘└────────────┘└┘   └────┘ └────────────────────────┘  └────┘
typ         └─────────┘└────────────┘└┘  └────┘ └────────────────────────┘└┘└────┘
doc         └─────────┘              └┘   └────┘                             └────┘
txt         └─────────┘              └┘   └────┘                             └────┘
par         └─────────┘              └┘   └────┘                             └────┘
pid             └──┘└┘              └┘                                     └───┘
st         └────────────────────────────────────────────────────────────────────────┘
 78    ⟨a, ha, ne_bot_of_le_ne_bot this (inf_le_inf ultrafilter_of_le (le_refl _))⟩⟩
id             └─────────────────┘ └──┘  └────────┘ └───────────────┘  └─────┘
src            └─────────────────┘       └────────┘ └───────────────┘  └─────┘
typ            └─────────────────┘ └──┘  └────────┘ └───────────────┘  └─────┘
 79  
 80  lemma compact.elim_finite_subcover {s : set α} {c : set (set α)}
id                                           └─┘        └─┘  └─┘ 
src                                          └─┘         └─┘  └─┘
typ                                          └─┘        └─┘  └─┘ 
 81    (hs : compact s) (hc₁ : ∀t∈c, is_open t) (hc₂ : s ⊆ ⋃₀ c) : ∃c'⊆c, finite c' ∧ s ⊆ ⋃₀ c' :=
id           └─────┘              └─────┘            └┘     └┘  └────┘ └┘    └┘ └┘
src          └─────┘                 └─────┘              └┘           └────┘        └┘
typ          └─────┘              └─────┘            └┘     └┘  └────┘ └┘    └┘ └┘
doc          └─────┘                 └─────┘                              └────┘
 82  classical.by_contradiction $ assume h,
id   └────────────────────────┘          
src  └────────────────────────┘
typ  └────────────────────────┘          
 83    have h : ∀{c'}, c' ⊆ c → finite c' → ¬ s ⊆ ⋃₀ c',
id                └┘   └┘     └────┘ └┘      └┘ └┘
src                            └────┘          └┘
typ               └┘   └┘     └────┘ └┘      └┘ └┘
doc                             └────┘
 84      from assume c' h₁ h₂ h₃, h ⟨c', h₁, h₂, h₃⟩,
id                   └┘ └┘ └┘ └┘    └┘  └┘  └┘  └┘
typ                  └┘ └┘ └┘ └┘    └┘  └┘  └┘  └┘
 85    let
id     └─┘
typ    └─┘
 86      f : filter α := (⨅c':{c' : set (set α) // c' ⊆ c ∧ finite c'}, principal (s - ⋃₀ c')),
id           └────┘              └─┘  └─┘      └┘    └────┘ └┘  └───────┘    └┘ └┘
src          └────┘               └─┘  └─┘              └────┘     └───────┘     └┘
typ          └────┘              └─┘  └─┘      └┘    └────┘ └┘  └───────┘    └┘ └┘
doc                                                        └────┘     └───────┘
 87      ⟨a, ha⟩ := (@ne_empty_iff_nonempty α s).1
id                   └───────────────────┘   
src                   └───────────────────┘     
typ                  └───────────────────┘   
 88        (assume h', h (empty_subset _) finite_empty $ h'.symm ▸ empty_subset _)
id                 └┘    └──────────┘    └──────────┘   └┘└───┘  └──────────┘
src                       └──────────┘    └──────────┘     └───┘  └──────────┘
typ                └┘    └──────────┘    └──────────┘   └┘└───┘  └──────────┘
 89    in
 90    have f ≠ ⊥, from infi_ne_bot_of_directed ⟨a⟩
id                   └─────────────────────┘
src                   └─────────────────────┘
typ                  └─────────────────────┘
doc                     └─────────────────────┘
 91      (assume ⟨c₁, hc₁, hc'₁⟩ ⟨c₂, hc₂, hc'₂⟩, ⟨⟨c₁ ∪ c₂, union_subset hc₁ hc₂, finite_union hc'₁ hc'₂⟩,
id               └┘  └─┘  └──┘  └┘  └─┘  └──┘             └──────────┘          └──────────┘
src                                                         └──────────┘          └──────────┘
typ              └┘  └─┘  └──┘  └┘  └─┘  └──┘             └──────────┘          └──────────┘
 92        principal_mono.mpr $ diff_subset_diff_right $ sUnion_mono $ subset_union_left _ _,
id         └────────────┘└──┘   └────────────────────┘   └─────────┘   └───────────────┘
src        └────────────┘└──┘   └────────────────────┘   └─────────┘   └───────────────┘
typ        └────────────┘└──┘   └────────────────────┘   └─────────┘   └───────────────┘
 93        principal_mono.mpr $ diff_subset_diff_right $ sUnion_mono $ subset_union_right _ _⟩)
id         └────────────┘└──┘   └────────────────────┘   └─────────┘   └────────────────┘
src        └────────────┘└──┘   └────────────────────┘   └─────────┘   └────────────────┘
typ        └────────────┘└──┘   └────────────────────┘   └─────────┘   └────────────────┘
 94      (assume ⟨c', hc'₁, hc'₂⟩, show principal (s \ _) ≠ ⊥, by simp only [ne.def, principal_eq_bot_iff, diff_eq_empty]; exact h hc'₁ hc'₂),
id                                     └───────┘                        └────┘  └──────────────────┘  └───────────┘          └──┘ └──┘
src                                     └───────┘              └─────────┘└────┘└┘└──────────────────┘└┘└───────────┘  └────┘     
typ                                    └───────┘             └─────────┘└────┘└┘└──────────────────┘└┘└───────────┘  └────┘└──┘└──┘
doc                                     └───────┘                 └─────────┘      └┘                    └┘               └────┘     
txt                                                               └─────────┘      └┘                    └┘               └────┘     
par                                                               └─────────┘      └┘                    └┘               └────┘     
pid                                                                   └──┘└┘      └┘                    └┘                         
st                                                               └─────────────────────────────────────────────────────────────────────────┘
 95    have f ≤ principal s, from infi_le_of_le ⟨∅, empty_subset _, finite_empty⟩ $
id            └───────┘        └───────────┘    └──────────┘    └──────────┘
src            └───────┘         └───────────┘    └──────────┘    └──────────┘
typ           └───────┘        └───────────┘    └──────────┘    └──────────┘
doc             └───────┘
 96      show principal (s \ ⋃₀∅) ≤ principal s, from le_principal_iff.2 (diff_subset _ _),
id            └───────┘    └┘   └───────┘        └──────────────┘   └─────────┘
src           └───────┘     └┘   └───────┘         └──────────────┘   └─────────┘
typ           └───────┘    └┘   └───────┘        └──────────────┘   └─────────┘
doc           └───────┘             └───────┘
 97    let
id     └─┘
typ    └─┘
 98      ⟨a, ha, (h : f ⊓ 𝓝 a ≠ ⊥)⟩ := hs f ‹f ≠ ⊥› this,
id          └┘                  └┘     └──┘
src                                        
typ         └┘                  └┘     └──┘
doc                                             
 99      ⟨t, ht₁, (ht₂ : a ∈ t)⟩ := hc₂ ha
id                                └─┘
src                        
typ                               └─┘
100    in
101    have f ≤ principal (-t),
id            └───────┘  
src            └───────┘  
typ           └───────┘  
doc             └───────┘
102      from infi_le_of_le ⟨{t}, by rwa singleton_subset_iff, finite_insert _ finite_empty⟩ $
id            └───────────┘             └──────────────────┘  └───────────┘   └──────────┘
src           └───────────┘         └──┘└──────────────────┘  └───────────┘   └──────────┘
typ           └───────────┘         └──┘└──────────────────┘  └───────────┘   └──────────┘
doc                                  └──┘
txt                                  └──┘
par                                  └──┘
pid                                     
st                                  └───────────────────────┘
103        principal_mono.mpr $
id         └────────────┘└──┘
src        └────────────┘└──┘
typ        └────────────┘└──┘
104          show s - ⋃₀{t} ⊆ - t, begin rw sUnion_singleton; exact assume x ⟨_, hnt⟩, hnt end,
id                  └┘                 └──────────────┘                     └─┘
src                  └┘              └─┘└──────────────┘  └────┘      └─────┘   └─┘   
typ                 └┘              └─┘└──────────────┘  └────┘      └─────┘└─┘└─┘   
doc                                      └─┘                  └────┘      └─────┘   └─┘   
txt                                      └─┘                  └────┘      └─────┘   └─┘   
par                                      └─┘                  └────┘      └─────┘   └─┘   
pid                                                                     └─────┘   └─┘   
st                                 └──────────────────────────────────────────────────────┘└─┘
105    have is_closed (- t), from is_open_compl_iff.mp $ by rw lattice.neg_neg; exact hc₁ t ht₁,
id          └───────┘            └───────────────┘└─┘         └─────────────┘        └─┘  └─┘
src         └───────┘            └───────────────┘└─┘      └─┘└─────────────┘  └────┘    
typ         └───────┘            └───────────────┘└─┘      └─┘└─────────────┘  └────┘└─┘└─┘
doc         └───────┘                                       └─┘                 └────┘    
txt                                                         └─┘                 └────┘    
par                                                         └─┘                 └────┘    
pid                                                                                     
st                                                         └──────────────────────────────────┘
106    have a ∈ - t, from is_closed_iff_nhds.mp this _ $ ne_bot_of_le_ne_bot h $
id                      └────────────────┘└─┘ └──┘     └─────────────────┘
src                     └────────────────┘└─┘          └─────────────────┘
typ                     └────────────────┘└─┘ └──┘     └─────────────────┘
107      le_inf inf_le_right (inf_le_left_of_le ‹f ≤ principal (- t)›),
id       └────┘ └──────────┘  └───────────────┘   └───────┘     
src      └────┘ └──────────┘  └───────────────┘    └───────┘     
typ      └────┘ └──────────┘  └───────────────┘   └───────┘     
doc                                                 └───────┘      
108    this ‹a ∈ t›
id     └──┘     
src             
typ    └──┘     
doc              
109  
110  lemma compact.elim_finite_subcover_image {s : set α} {b : set β} {c : β → set α}
id                                                 └─┘        └─┘           └─┘ 
src                                                └─┘         └─┘             └─┘
typ                                                └─┘        └─┘           └─┘ 
111    (hs : compact s) (hc₁ : ∀i∈b, is_open (c i)) (hc₂ : s ⊆ ⋃i∈b, c i) :
id           └─────┘              └─────┘                  
src          └─────┘                 └─────┘                     
typ          └─────┘              └─────┘                  
doc          └─────┘                 └─────┘                      
112    ∃b'⊆b, finite b' ∧ s ⊆ ⋃i∈b', c i :=
id     └┘  └────┘ └┘     └┘  
src         └────┘            
typ    └┘  └────┘ └┘     └┘  
doc           └────┘              
113  b.eq_empty_or_nonempty.elim (λ h, ⟨∅, empty_subset _, finite_empty, h ▸ hc₂⟩) $
id   └───────────────────┘└───┘         └──────────┘    └──────────┘    └─┘
src   └───────────────────┘└───┘          └──────────┘    └──────────┘    
typ  └───────────────────┘└───┘         └──────────┘    └──────────┘    └─┘
114  assume ⟨i, hi⟩,
id          
typ         
115  have hc'₁ : ∀i∈c '' b, is_open i, from assume i ⟨j, hj, h⟩, h ▸ hc₁ _ hj,
id                  └┘   └─────┘                   └┘        └─┘
src                   └┘    └─────┘                                
typ                 └┘   └─────┘                   └┘        └─┘
doc                         └─────┘
116  have hc'₂ : s ⊆ ⋃₀ (c '' b), by rwa set.sUnion_image,
id                 └┘   └┘           └──────────────┘
src                 └┘    └┘        └──┘└──────────────┘
typ                └┘   └┘       └──┘└──────────────┘
doc                                  └──┘
txt                                  └──┘
par                                  └──┘
pid                                     
st                                  └───────────────────┘
117  let ⟨d, hd₁, hd₂, hd₃⟩ := hs.elim_finite_subcover hc'₁ hc'₂ in
id   └─┘    └─┘  └─┘  └─┘     └┘└───────────────────┘ └──┘ └──┘
src                              └───────────────────┘
typ  └─┘    └─┘  └─┘  └─┘     └┘└───────────────────┘ └──┘ └──┘
118  have ∀x : d, ∃i, i ∈ b ∧ c i = x, from assume ⟨x, hx⟩, hd₁ hx,
id                                         └┘
src                           
typ                                        └┘
119  let ⟨f', hf⟩ := axiom_of_choice this,
id   └─┘  └┘         └─────────────┘ └──┘
src                  └─────────────┘
typ  └─┘  └┘         └─────────────┘ └──┘
120      f := λx:set α, (if h : x ∈ d then f' ⟨x, h⟩ else i : β) in
id              └─┘    └┘                              
src              └─┘     └┘                              
typ             └─┘    └┘                              
121  have ∀(x : α) (i : set α), i ∈ d → x ∈ i → (∃ (i : β), i ∈ f '' d ∧ x ∈ c i),
id                     └─┘                           └┘       
src                     └─┘                                  └┘      
typ                    └─┘                           └┘       
122    from assume x i hid hxi, ⟨f i, mem_image_of_mem f hid,
id                   └─┘ └─┘      └──────────────┘  └─┘
src                                   └──────────────┘
typ                  └─┘ └─┘      └──────────────┘  └─┘
123      by simpa only [f, dif_pos hid, (hf ⟨_, hid⟩).2] using hxi⟩,
id                        └─────┘ └─┘   └┘     └─┘            └─┘
src         └──────────┘ └┘└─────┘   └┘    └─┘   └──────────┘
typ         └──────────┘└┘└─────┘└─┘└┘ └┘ └─┘└─┘└──────────┘└─┘
doc         └──────────┘ └┘          └┘    └─┘   └──────────┘
txt         └──────────┘ └┘          └┘    └─┘   └──────────┘
par         └──────────┘ └┘          └┘    └─┘   └──────────┘
pid              └──┘└┘ └┘          └┘    └─┘   └───┘└────┘
st         └─────────────────────────────────────────────────────┘
124  ⟨f '' d,
id     └┘
src     └┘
typ    └┘
125    assume i ⟨j, hj, h⟩,
id                    
typ                   
126    h ▸ by simpa only [f, dif_pos hj] using (hf ⟨_, hj⟩).1,
id                         └─────┘ └┘         └┘     └┘
src          └──────────┘ └┘└─────┘  └──────┘    └─┘  └──┘
typ          └──────────┘└┘└─────┘└┘└──────┘ └┘ └─┘└┘└──┘
doc           └──────────┘ └┘         └──────┘    └─┘  └──┘
txt           └──────────┘ └┘         └──────┘    └─┘  └──┘
par           └──────────┘ └┘         └──────┘    └─┘  └──┘
pid                └──┘└┘ └┘         └────┘    └─┘  └┘└┘
st           └──────────────────────────────────────────────┘
127    finite_image f hd₂,
id     └──────────┘ 
src    └──────────┘
typ    └──────────┘ 
128    subset.trans hd₃ $ by simpa only [subset_def, mem_sUnion, exists_imp_distrib, mem_Union, exists_prop, and_imp]⟩
id     └──────────┘                      └────────┘  └────────┘  └────────────────┘  └───────┘  └─────────┘  └─────┘
src    └──────────┘          └──────────┘└────────┘└┘└────────┘└┘└────────────────┘└┘└───────┘└┘└─────────┘└┘└─────┘
typ    └──────────┘          └──────────┘└────────┘└┘└────────┘└┘└────────────────┘└┘└───────┘└┘└─────────┘└┘└─────┘
doc                          └──────────┘          └┘          └┘                  └┘         └┘           └┘       
txt                          └──────────┘          └┘          └┘                  └┘         └┘           └┘       
par                          └──────────┘          └┘          └┘                  └┘         └┘           └┘       
pid                               └──┘└┘          └┘          └┘                  └┘         └┘           └┘       
st                          └───────────────────────────────────────────────────────────────────────────────────────┘
129  
130  section
131  -- this proof times out without this
132  local attribute [instance, priority 1000] classical.prop_decidable
id                                             └──────────────────────┘
src                                            └──────────────────────┘
typ                                            └──────────────────────┘
133  lemma compact_of_finite_subcover {s : set α}
id                                         └─┘ 
src                                        └─┘
typ                                        └─┘ 
134    (h : ∀c, (∀t∈c, is_open t) → s ⊆ ⋃₀ c → ∃c'⊆c, finite c' ∧ s ⊆ ⋃₀ c') : compact s :=
id                  └─────┘       └┘    └┘  └────┘ └┘    └┘ └┘    └─────┘ 
src                    └─────┘         └┘          └────┘        └┘       └─────┘
typ                 └─────┘       └┘    └┘  └────┘ └┘    └┘ └┘    └─────┘ 
doc                    └─────┘                        └────┘                   └─────┘
135  assume f hfn hfs, classical.by_contradiction $ assume : ¬ (∃x∈s, f ⊓ 𝓝 x ≠ ⊥),
id           └─┘ └─┘  └────────────────────────┘                     
src                    └────────────────────────┘                         
typ          └─┘ └─┘  └────────────────────────┘                     
doc                                                                       
136    have hf : ∀x∈s, 𝓝 x ⊓ f = ⊥,
id                        
src                           
typ                       
doc                    
137      by simpa only [not_exists, not_not, inf_comm],
id                      └────────┘  └─────┘  └──────┘
src         └──────────┘└────────┘└┘└─────┘└┘└──────┘
typ         └──────────┘└────────┘└┘└─────┘└┘└──────┘
doc         └──────────┘          └┘       └┘        
txt         └──────────┘          └┘       └┘        
par         └──────────┘          └┘       └┘        
pid              └──┘└┘          └┘       └┘        
st         └─────────────────────────────────────────┘
138    have ¬ ∃x∈s, ∀t∈f.sets, x ∈ closure t,
id               └───┘    └─────┘ 
src                  └───┘     └─────┘
typ              └───┘    └─────┘ 
doc                                └─────┘
139      from assume ⟨x, hxs, hx⟩,
id                   
typ                  
140      have ∅ ∈ 𝓝 x ⊓ f, by rw [empty_in_sets_eq_bot, hf x hxs],
id                           └──────────────────┘  └┘  └─┘
src                       └──┘└──────────────────┘└┘      
typ                      └──┘└──────────────────┘└┘└┘└─┘
doc                          └──┘                    └┘      
txt                           └──┘                    └┘      
par                           └──┘                    └┘      
pid                             └┘                    └┘      
st                           └───────────────────────┘└────────┘
141      let ⟨t₁, ht₁, t₂, ht₂, ht⟩ := by rw [mem_inf_sets] at this; exact this in
id       └─┘      └─┘  └┘       └┘            └──────────┘                 └──┘
src                                       └──┘└──────────┘└───────┘  └────┘    
typ      └─┘      └─┘  └┘       └┘        └──┘└──────────┘└───────┘  └────┘└──┘
doc                                       └──┘            └───────┘  └────┘    
txt                                       └──┘            └───────┘  └────┘    
par                                       └──┘            └───────┘  └────┘    
pid                                         └┘            └──────┘           
st                                       └───────────────┘└───────────────────┘
142      have ∅ ∈ 𝓝 x ⊓ principal t₂,
id                  └───────┘
src                 └───────┘
typ                 └───────┘
doc                    └───────┘
143        from (𝓝 x ⊓ principal t₂).sets_of_superset (inter_mem_inf_sets ht₁ (subset.refl t₂)) ht,
id                   └───────┘    └──────────────┘   └────────────────┘      └─────────┘
src                  └───────┘    └──────────────┘   └────────────────┘      └─────────┘
typ                  └───────┘    └──────────────┘   └────────────────┘      └─────────┘
doc                   └───────┘
144      have 𝓝 x ⊓ principal t₂ = ⊥,
id                └───────┘     
src               └───────┘     
typ               └───────┘     
doc                └───────┘
145        by rwa [empty_in_sets_eq_bot] at this,
id                 └──────────────────┘
src           └───┘└──────────────────┘└───────┘
typ           └───┘└──────────────────┘└───────┘
doc           └───┘                    └───────┘
txt           └───┘                    └───────┘
par           └───┘                    └───────┘
pid              └┘                    └──────┘
st           └────────────────────────┘└──────┘
146      by simp only [closure_eq_nhds] at hx; exact hx t₂ ht₂ this,
id                     └─────────────┘               └┘ └┘ └─┘ └──┘
src         └─────────┘└─────────────┘└─────┘  └────┘       
typ         └─────────┘└─────────────┘└─────┘  └────┘└┘└┘└─┘└──┘
doc         └─────────┘               └─────┘  └────┘       
txt         └─────────┘               └─────┘  └────┘       
par         └─────────┘               └─────┘  └────┘       
pid             └──┘└┘               └───┘              
st         └──────────────────────────────────────────────────────┘
147    have ∀x∈s, ∃t∈f.sets, x ∉ closure t, by simpa only [not_exists, not_forall],
id               └───┘   └─────┘                  └────────┘  └────────┘
src                  └───┘    └─────┘       └──────────┘└────────┘└┘└────────┘
typ              └───┘   └─────┘      └──────────┘└────────┘└┘└────────┘
doc                              └─────┘       └──────────┘          └┘          
txt                                            └──────────┘          └┘          
par                                            └──────────┘          └┘          
pid                                                 └──┘└┘          └┘          
st                                            └──────────────────────────────────┘
148    let c := (λt, - closure t) '' f.sets, ⟨c', hcc', hcf, hsc'⟩ := h c
id     └─┘          └─────┘   └┘ └───┘   └┘  └──┘  └─┘  └──┘      
src                   └─────┘    └┘  └───┘
typ    └─┘          └─────┘   └┘ └───┘   └┘  └──┘  └─┘  └──┘      
doc                    └─────┘
149      (assume t ⟨s, hs, h⟩, h ▸ is_closed_closure) (by simpa only [subset_def, sUnion_image, mem_Union]) in
id                             └───────────────┘                  └────────┘  └──────────┘  └───────┘
src                               └───────────────┘      └──────────┘└────────┘└┘└──────────┘└┘└───────┘
typ                            └───────────────┘      └──────────┘└────────┘└┘└──────────┘└┘└───────┘
doc                                                       └──────────┘          └┘            └┘         
txt                                                       └──────────┘          └┘            └┘         
par                                                       └──────────┘          └┘            └┘         
pid                                                            └──┘└┘          └┘            └┘         
st                                                       └───────────────────────────────────────────────┘
150    let ⟨b, hb⟩ := axiom_of_choice $
id     └─┘    └┘     └─────────────┘
src                   └─────────────┘
typ    └─┘    └┘     └─────────────┘
151      show ∀s:c', ∃t, t ∈ f ∧ - closure t = s,
id                        └─────┘   
src                           └─────┘   
typ                       └─────┘   
doc                                └─────┘
152        from assume ⟨x, hx⟩, hcc' hx in
id                        └┘
typ                       └┘
153    have (⋂s∈c', if h : s ∈ c' then b ⟨s, h⟩ else univ) ∈ f,
id               └┘                           └──┘   
src               └┘                              └──┘  
typ              └┘                           └──┘   
doc              
154      from Inter_mem_sets hcf $ assume t ht, by rw [dif_pos ht]; exact (hb ⟨t, ht⟩).left,
id            └────────────┘               └┘         └─────┘ └┘          └┘    └┘
src           └────────────┘                       └──┘└─────┘    └────┘     └┘  └─────┘
typ           └────────────┘               └┘     └──┘└─────┘└┘  └────┘ └┘ └┘└┘└─────┘
doc                                                └──┘           └────┘     └┘  └─────┘
txt                                                └──┘           └────┘     └┘  └─────┘
par                                                └──┘           └────┘     └┘  └─────┘
pid                                                  └┘                     └┘  └────┘
st                                                └─────────────┘└───────────────────────┘
155    have s ∩ (⋂s∈c', if h : s ∈ c' then b ⟨s, h⟩ else univ) ∈ f,
id                 └┘                           └──┘   
src                  └┘                              └──┘  
typ                └┘                           └──┘   
doc                  
156      from inter_mem_sets (le_principal_iff.1 hfs) this,
id            └────────────┘  └──────────────┘  └─┘  └──┘
src           └────────────┘  └──────────────┘
typ           └────────────┘  └──────────────┘  └─┘  └──┘
157    have ∅ ∈ f,
id            
src          
typ           
158      from mem_sets_of_superset this $ assume x ⟨hxs, hxi⟩,
id            └──────────────────┘ └──┘           └─┘
src           └──────────────────┘
typ           └──────────────────┘ └──┘           └─┘
159      let ⟨t, htc', hxt⟩ := (show ∃t ∈ c', x ∈ t, from hsc' hxs) in
id       └─┘    └──┘  └─┘                   
src                                           
typ      └─┘    └──┘  └─┘                   
160      have -closure (b ⟨t, htc'⟩) = t, from (hb _).right,
id            └─────┘                              └───┘
src           └─────┘                              └───┘
typ           └─────┘                              └───┘
doc            └─────┘
161      have x ∈ - t,
id              
src              
typ             
162        from this ▸ (calc x ∈ b ⟨t, htc'⟩ : by rw mem_bInter_iff at hxi; have h := hxi t htc'; rwa [dif_pos htc'] at h
id              └──┘                               └────────────┘                   └─┘  └──┘       └─────┘ └──┘
src                                              └─┘└────────────┘└─────┘  └────────┘          └───┘└─────┘    └──────
typ             └──┘                            └─┘└────────────┘└─────┘  └────────┘└─┘└──┘  └───┘└─────┘└──┘└──────
doc                                               └─┘              └─────┘  └────────┘          └───┘           └──────
txt                                               └─┘              └─────┘  └────────┘          └───┘           └──────
par                                               └─┘              └─────┘  └────────┘          └───┘           └──────
pid                                                               └─────┘  └────┘└─┘             └┘           └───┘
st                                               └────────────────────────────────────────────────────┘└──────────┘└─────
163          ... ⊆ closure (b ⟨t, htc'⟩) : subset_closure
id                 └─────┘                 └────────────┘
src  ───────┘      └─────┘                 └────────────┘
typ  ───────┘      └─────┘                 └────────────┘
doc  ───────┘      └─────┘
txt  ───────┘
par  ───────┘
pid  ───────┘
st   ───────┘
164          ... ⊆ - - closure (b ⟨t, htc'⟩) : by rw lattice.neg_neg; exact subset.refl _),
id                   └─────┘                       └─────────────┘        └─────────┘
src                  └─────┘                    └─┘└─────────────┘  └────┘└─────────┘└┘
typ                  └─────┘                    └─┘└─────────────┘  └────┘└─────────┘└┘
doc                    └─────┘                    └─┘                 └────┘           └┘
txt                                               └─┘                 └────┘           └┘
par                                               └─┘                 └────┘           └┘
pid                                                                                  └┘
st                                               └──────────────────────────────────────┘
165      show false, from this hxt,
id            └───┘       └──┘
src           └───┘
typ           └───┘       └──┘
166    hfn $ by rwa [empty_in_sets_eq_bot] at this
id     └─┘           └──────────────────┘
src             └───┘└──────────────────┘└────────┘
typ    └─┘      └───┘└──────────────────┘└────────┘
doc             └───┘                    └────────┘
txt             └───┘                    └────────┘
par             └───┘                    └────────┘
pid                └┘                    └──────┘
st             └────────────────────────┘└───────┘
167  end
168  
169  lemma compact_iff_finite_subcover {s : set α} :
id                                          └─┘ 
src                                         └─┘
typ                                         └─┘ 
170    compact s ↔ (∀c, (∀t∈c, is_open t) → s ⊆ ⋃₀ c → ∃c'⊆c, finite c' ∧ s ⊆ ⋃₀ c') :=
id     └─────┘            └─────┘       └┘    └┘  └────┘ └┘    └┘ └┘
src    └─────┘                └─────┘         └┘          └────┘        └┘
typ    └─────┘            └─────┘       └┘    └┘  └────┘ └┘    └┘ └┘
doc    └─────┘                 └─────┘                        └────┘
171  ⟨assume hc c, hc.elim_finite_subcover, compact_of_finite_subcover⟩
id           └┘   └┘└───────────────────┘  └────────────────────────┘
src                  └───────────────────┘  └────────────────────────┘
typ          └┘   └┘└───────────────────┘  └────────────────────────┘
172  
173  @[simp]
doc    └──┘
174  lemma compact_empty : compact (∅ : set α) :=
id                         └─────┘     └─┘ 
src                        └─────┘     └─┘
typ                        └─────┘     └─┘ 
doc                        └─────┘
175  assume f hnf hsf, not.elim hnf $
id           └─┘ └─┘  └──────┘ └─┘
src                    └──────┘
typ          └─┘ └─┘  └──────┘ └─┘
176  empty_in_sets_eq_bot.1 $ le_principal_iff.1 hsf
id   └──────────────────┘    └──────────────┘  └─┘
src  └──────────────────┘    └──────────────┘
typ  └──────────────────┘    └──────────────┘  └─┘
177  
178  @[simp]
doc    └──┘
179  lemma compact_singleton {a : α} : compact ({a} : set α) :=
id                                    └─────┘      └─┘ 
src                                    └─────┘       └─┘
typ                                   └─────┘      └─┘ 
doc                                    └─────┘
180  compact_of_finite_subcover $ assume c hc₁ hc₂,
id   └────────────────────────┘           └─┘ └─┘
src  └────────────────────────┘
typ  └────────────────────────┘           └─┘ └─┘
181    let ⟨i, hic, hai⟩ := (show ∃i ∈ c, a ∈ i, from mem_sUnion.1 $ singleton_subset_iff.1 hc₂) in
id     └─┘    └─┘                             └────────┘    └──────────────────┘  └─┘
src                                                └────────┘    └──────────────────┘
typ    └─┘    └─┘                             └────────┘    └──────────────────┘  └─┘
182    ⟨{i}, singleton_subset_iff.2 hic, finite_singleton _, by rwa [sUnion_singleton, singleton_subset_iff]⟩
id          └──────────────────┘       └──────────────┘            └──────────────┘  └──────────────────┘
src         └──────────────────┘       └──────────────┘       └───┘└──────────────┘└┘└──────────────────┘
typ         └──────────────────┘       └──────────────┘       └───┘└──────────────┘└┘└──────────────────┘
doc                                                             └───┘                └┘                    
txt                                                             └───┘                └┘                    
par                                                             └───┘                └┘                    
pid                                                                └┘                └┘                    
st                                                             └────────────────────┘└────────────────────┘
183  
184  lemma set.finite.compact_bUnion {s : set β} {f : β → set α} (hs : finite s) :
id                                        └─┘           └─┘         └────┘ 
src                                       └─┘             └─┘          └────┘
typ                                       └─┘           └─┘         └────┘ 
doc                                                                    └────┘
185    (∀i ∈ s, compact (f i)) → compact (⋃i ∈ s, f i) :=
id            └─────┘        └─────┘       
src             └─────┘          └─────┘       
typ           └─────┘        └─────┘       
doc             └─────┘          └─────┘       
186  assume hf, compact_of_finite_subcover $ assume c c_open c_cover,
id          └┘  └────────────────────────┘           └────┘ └─────┘
src             └────────────────────────┘
typ         └┘  └────────────────────────┘           └────┘ └─────┘
187    have ∀i : subtype s, ∃c' ⊆ c, finite c' ∧ f i ⊆ ⋃₀ c', from
id               └─────┘   └┘    └────┘ └┘     └┘ └┘
src              └─────┘           └────┘          └┘
typ              └─────┘   └┘    └────┘ └┘     └┘ └┘
doc                                  └────┘
188      assume ⟨i, hi⟩, (hf i hi).elim_finite_subcover c_open
id                └┘    └┘      └──────────────────┘  └────┘
src                               └──────────────────┘
typ               └┘    └┘      └──────────────────┘  └────┘
189        (calc f i ⊆ ⋃i ∈ s, f i : subset_bUnion_of_mem hi
id                            └──────────────────┘
src                                └──────────────────┘
typ                           └──────────────────┘
doc                         
190              ... ⊆ ⋃₀ c        : c_cover),
id                     └┘           └─────┘
src                    └┘
typ                    └┘           └─────┘
191    let ⟨finite_subcovers, h⟩ := axiom_of_choice this in
id     └─┘  └──────────────┘       └─────────────┘ └──┘
src                                 └─────────────┘
typ    └─┘  └──────────────┘       └─────────────┘ └──┘
192    let c' := ⋃i, finite_subcovers i in
id         └┘                      
src               
typ        └┘                      
doc               
193    have c' ⊆ c, from Union_subset (λi, (h i).fst),
id          └┘         └──────────┘         └─┘
src                     └──────────┘           └─┘
typ         └┘         └──────────┘         └─┘
194    have finite c', from @finite_Union _ _ hs.fintype _ (λi, (h i).snd.1),
id          └────┘ └┘        └──────────┘     └┘└──────┘           └─┘ 
src         └────┘           └──────────┘       └──────┘             └─┘ 
typ         └────┘ └┘        └──────────┘     └┘└──────┘           └─┘ 
doc         └────┘                              └──────┘
195    have (⋃i ∈ s, f i) ⊆ ⋃₀ c', from bUnion_subset $ λi hi, calc
id                   └┘ └┘       └───────────┘     └┘
src                      └┘          └───────────┘
typ                  └┘ └┘       └───────────┘     └┘
doc               
196      f i ⊆ ⋃₀ finite_subcovers ⟨i,hi⟩ : (h ⟨i,hi⟩).snd.2
id           └┘                    └┘         └┘  └─┘ 
src            └┘                                     └─┘ 
typ          └┘                    └┘         └┘  └─┘ 
197      ... ⊆ ⋃₀ c'                      : sUnion_mono (subset_Union _ _),
id             └┘ └┘                        └─────────┘  └──────────┘
src            └┘                           └─────────┘  └──────────┘
typ            └┘ └┘                        └─────────┘  └──────────┘
198    ⟨c', ‹c' ⊆ c›, ‹finite c'›, this⟩
id      └┘  └┘    └────┘ └┘  └──┘
src                └────┘   
typ     └┘  └┘    └────┘ └┘  └──┘
doc                 └────┘   
199  
200  lemma compact_Union {f : β → set α} [fintype β]
id                               └─┘    └─────┘ 
src                               └─┘     └─────┘
typ                              └─┘    └─────┘ 
doc                                       └─────┘
201    (h : ∀i, compact (f i)) : compact (⋃i, f i) :=
id             └─────┘        └─────┘    
src             └─────┘          └─────┘   
typ            └─────┘        └─────┘    
doc             └─────┘          └─────┘   
202  by rw ← bUnion_univ; exact finite_univ.compact_bUnion (λ i _, h i)
id           └─────────┘        └────────────────────────┘         
src     └───┘└─────────┘  └────┘└────────────────────────┘  └────┘  └─
typ     └───┘└─────────┘  └────┘└────────────────────────┘  └────┘ └─
doc     └───┘             └────┘                            └────┘  └─
txt     └───┘             └────┘                            └────┘  └─
par     └───┘             └────┘                            └────┘  └─
pid       └─┘                                              └────┘  
st     └────────────────────────────────────────────────────────────────
203  
src  
typ  
doc  
txt  
par  
pid  
st   
204  lemma set.finite.compact {s : set α} (hs : finite s) : compact s :=
id                                 └─┘         └────┘     └─────┘ 
src                                └─┘          └────┘      └─────┘
typ                                └─┘         └────┘     └─────┘ 
doc                                             └────┘      └─────┘
205  bUnion_of_singleton s ▸ hs.compact_bUnion (λ _ _, compact_singleton)
id   └─────────────────┘   └┘└─────────────┘       └───────────────┘
src  └─────────────────┘      └─────────────┘         └───────────────┘
typ  └─────────────────┘   └┘└─────────────┘       └───────────────┘
206  
207  lemma compact.union {s t : set α} (hs : compact s) (ht : compact t) : compact (s ∪ t) :=
id                              └─┘         └─────┘         └─────┘     └─────┘    
src                             └─┘          └─────┘          └─────┘      └─────┘    
typ                             └─┘         └─────┘         └─────┘     └─────┘    
doc                                          └─────┘          └─────┘      └─────┘
208  by rw union_eq_Union; exact compact_Union (λ b, by cases b; assumption)
id         └────────────┘        └───────────┘                
src     └─┘└────────────┘  └────┘└───────────┘  └──┘  └────┘ └┘└────────┘└─
typ     └─┘└────────────┘  └────┘└───────────┘  └──┘  └────┘└┘└────────┘└─
doc     └─┘                └────┘               └──┘  └────┘ └┘└────────┘└─
txt     └─┘                └────┘               └──┘  └────┘ └┘└────────┘└─
par     └─┘                └────┘               └──┘  └────┘ └┘└────────┘└─
pid                                           └──┘  └─────┘ └───────────┘
st     └──────────────────────────────────────────────┘└──────────────────┘└─
209  
src  
typ  
doc  
txt  
par  
pid  
st   
210  section tube_lemma
211  
212  variables [topological_space β]
id              └───────────────┘
src             └───────────────┘
typ             └───────────────┘
doc             └───────────────┘
213  
214  /-- `nhds_contain_boxes s t` means that any open neighborhood of `s × t` in `α × β` includes
215  a product of an open neighborhood of `s` by an open neighborhood of `t`. -/
216  def nhds_contain_boxes (s : set α) (t : set β) : Prop :=
id                               └─┘        └─┘ 
src                              └─┘         └─┘
typ                              └─┘        └─┘ 
217  ∀ (n : set (α × β)) (hn : is_open n) (hp : set.prod s t ⊆ n),
id          └─┘             └─────┘         └──────┘    
src         └─┘               └─────┘          └──────┘     
typ         └─┘             └─────┘         └──────┘    
doc                            └─────┘          └──────┘
218  ∃ (u : set α) (v : set β), is_open u ∧ is_open v ∧ s ⊆ u ∧ t ⊆ v ∧ set.prod u v ⊆ n
id         └─┘        └─┘   └─────┘   └─────┘           └──────┘    
src        └─┘         └─┘    └─────┘    └─────┘                └──────┘     
typ        └─┘        └─┘   └─────┘   └─────┘           └──────┘    
doc                             └─────┘     └─────┘                     └──────┘
219  
220  lemma nhds_contain_boxes.symm {s : set α} {t : set β} :
id                                      └─┘        └─┘ 
src                                     └─┘         └─┘
typ                                     └─┘        └─┘ 
221    nhds_contain_boxes s t → nhds_contain_boxes t s :=
id     └────────────────┘     └────────────────┘  
src    └────────────────┘       └────────────────┘
typ    └────────────────┘     └────────────────┘  
doc    └────────────────┘       └────────────────┘
222  assume H n hn hp,
id            └┘ └┘
typ           └┘ └┘
223    let ⟨u, v, uo, vo, su, tv, p⟩ :=
id     └─┘      └┘  └┘  └┘  └┘
typ    └─┘      └┘  └┘  └┘  └┘
224      H (prod.swap ⁻¹' n)
id         └───────┘ └─┘ 
src         └───────┘ └─┘
typ        └───────┘ └─┘ 
doc         └───────┘ └─┘
225        (continuous_swap n hn)
id          └─────────────┘  └┘
src         └─────────────┘
typ         └─────────────┘  └┘
226        (by rwa [←image_subset_iff, prod.swap, image_swap_prod]) in
id                   └──────────────┘  └───────┘  └─────────────┘
src            └────┘└──────────────┘└┘└───────┘└┘└─────────────┘
typ            └────┘└──────────────┘└┘└───────┘└┘└─────────────┘
doc            └────┘└──────────────┘└┘└───────┘└┘               
txt            └────┘                └┘         └┘               
par            └────┘                └┘         └┘               
pid               └─┘                └┘         └┘               
st            └─────────────────────┘└─────────┘└───────────────┘
227    ⟨v, u, vo, uo, tv, su,
228      by rwa [←image_subset_iff, prod.swap, image_swap_prod] at p⟩
id                └──────────────┘  └───────┘  └─────────────┘
src         └────┘└──────────────┘└┘└───────┘└┘└─────────────┘└────┘
typ         └────┘└──────────────┘└┘└───────┘└┘└─────────────┘└────┘
doc         └────┘└──────────────┘└┘└───────┘└┘               └────┘
txt         └────┘                └┘         └┘               └────┘
par         └────┘                └┘         └┘               └────┘
pid            └─┘                └┘         └┘               └───┘
st         └─────────────────────┘└─────────┘└───────────────┘└───┘
229  
230  lemma nhds_contain_boxes.comm {s : set α} {t : set β} :
id                                      └─┘        └─┘ 
src                                     └─┘         └─┘
typ                                     └─┘        └─┘ 
231    nhds_contain_boxes s t ↔ nhds_contain_boxes t s :=
id     └────────────────┘    └────────────────┘  
src    └────────────────┘      └────────────────┘
typ    └────────────────┘    └────────────────┘  
doc    └────────────────┘       └────────────────┘
232  iff.intro nhds_contain_boxes.symm nhds_contain_boxes.symm
id   └───────┘ └─────────────────────┘ └─────────────────────┘
src  └───────┘ └─────────────────────┘ └─────────────────────┘
typ  └───────┘ └─────────────────────┘ └─────────────────────┘
233  
234  lemma nhds_contain_boxes_of_singleton {x : α} {y : β} :
id                                                     
typ                                                    
235    nhds_contain_boxes ({x} : set α) ({y} : set β) :=
id     └────────────────┘      └─┘        └─┘ 
src    └────────────────┘       └─┘          └─┘
typ    └────────────────┘      └─┘        └─┘ 
doc    └────────────────┘
236  assume n hn hp,
id           └┘ └┘
typ          └┘ └┘
237    let ⟨u, v, uo, vo, xu, yv, hp'⟩ :=
id     └─┘      └┘  └┘          └─┘
typ    └─┘      └┘  └┘          └─┘
238      is_open_prod_iff.mp hn x y (hp $ by simp) in
id       └──────────────┘└─┘ └┘    └┘
src      └──────────────┘└─┘                 └──┘
typ      └──────────────┘└─┘ └┘    └┘      └──┘
doc                                          └──┘
txt                                          └──┘
par                                          └──┘
st                                          └───┘
239    ⟨u, v, uo, vo, by simpa, by simpa, hp'⟩
src                      └───┘     └───┘
typ                      └───┘     └───┘
doc                      └───┘     └───┘
txt                      └───┘     └───┘
par                      └───┘     └───┘
st                      └────┘    └────┘
240  
241  lemma nhds_contain_boxes_of_compact {s : set α} (hs : compact s) (t : set β)
id                                            └─┘         └─────┘        └─┘ 
src                                           └─┘          └─────┘         └─┘
typ                                           └─┘         └─────┘        └─┘ 
doc                                                        └─────┘
242    (H : ∀ x ∈ s, nhds_contain_boxes ({x} : set α) t) : nhds_contain_boxes s t :=
id                 └────────────────┘      └─┘       └────────────────┘  
src                  └────────────────┘       └─┘         └────────────────┘
typ                └────────────────┘      └─┘       └────────────────┘  
doc                  └────────────────┘                    └────────────────┘
243  assume n hn hp,
id           └┘ └┘
typ          └┘ └┘
244  have ∀x : subtype s, ∃uv : set α × set β,
id             └─────┘        └─┘   └─┘ 
src            └─────┘         └─┘    └─┘  
typ            └─────┘        └─┘   └─┘ 
245       is_open uv.1 ∧ is_open uv.2 ∧ {↑x} ⊆ uv.1 ∧ t ⊆ uv.2 ∧ set.prod uv.1 uv.2 ⊆ n,
id        └─────┘ └┘   └─────┘ └┘      └┘     └┘   └──────┘ └┘  └┘   
src       └─────┘      └─────┘                       └──────┘         
typ       └─────┘ └┘   └─────┘ └┘      └┘     └┘   └──────┘ └┘  └┘   
doc       └─────┘        └─────┘                                 └──────┘
246    from assume ⟨x, hx⟩,
id                   └┘
typ                  └┘
247      have set.prod {x} t ⊆ n, from
id            └──────┘      
src           └──────┘      
typ           └──────┘      
doc           └──────┘
248        subset.trans (prod_mono (by simpa) (subset.refl _)) hp,
id         └──────────┘  └───────┘             └─────────┘     └┘
src        └──────────┘  └───────┘     └───┘   └─────────┘
typ        └──────────┘  └───────┘     └───┘   └─────────┘     └┘
doc                                    └───┘
txt                                    └───┘
par                                    └───┘
st                                    └────┘
249      let ⟨ux,vx,H1⟩ := H x hx n hn this in ⟨⟨ux,vx⟩,H1⟩,
id       └─┘  └┘ └┘ └┘            └┘ └──┘
typ      └─┘  └┘ └┘ └┘            └┘ └──┘
250  let ⟨uvs, h⟩ := classical.axiom_of_choice this in
id   └─┘  └─┘       └───────────────────────┘ └──┘
src                  └───────────────────────┘
typ  └─┘  └─┘       └───────────────────────┘ └──┘
251  have us_cover : s ⊆ ⋃i, (uvs i).1, from
id                            
src                              
typ                           
doc                       
252    assume x hx, set.subset_Union _ ⟨x,hx⟩ (by simpa using (h ⟨x,hx⟩).2.2.1),
id             └┘  └──────────────┘     └┘                      └┘
src                 └──────────────┘              └──────────┘      └──────┘
typ            └┘  └──────────────┘     └┘      └──────────┘  └┘└──────┘
doc                                               └──────────┘      └──────┘
txt                                               └──────────┘      └──────┘
par                                               └──────────┘      └──────┘
pid                                                    └────┘      └────┘└┘
st                                               └───────────────────────────┘
253  let ⟨s0, _, s0_fin, s0_cover⟩ :=
id   └─┘  └┘     └────┘  └──────┘
typ  └─┘  └┘     └────┘  └──────┘
254    hs.elim_finite_subcover_image (λi _, (h i).1) $
id     └┘└─────────────────────────┘          
src      └─────────────────────────┘             
typ    └┘└─────────────────────────┘          
255      by rw bUnion_univ; exact us_cover in
id             └─────────┘        └──────┘
src         └─┘└─────────┘  └────┘        
typ         └─┘└─────────┘  └────┘└──────┘
doc         └─┘             └────┘        
txt         └─┘             └────┘        
par         └─┘             └────┘        
pid                                     
st         └──────────────────────────────┘
256  let u := ⋃(i ∈ s0), (uvs i).1 in
id                         
src                           
typ                        
doc                   
257  let v := ⋂(i ∈ s0), (uvs i).2 in
id                         
src                           
typ                        
doc                   
258  have is_open u, from is_open_bUnion (λi _, (h i).1),
id        └─────┘        └────────────┘          
src       └─────┘         └────────────┘             
typ       └─────┘        └────────────┘          
doc       └─────┘
259  have is_open v, from is_open_bInter s0_fin (λi _, (h i).2.1),
id        └─────┘        └────────────┘                  
src       └─────┘         └────────────┘                     
typ       └─────┘        └────────────┘                  
doc       └─────┘
260  have t ⊆ v, from subset_bInter (λi _, (h i).2.2.2.1),
id                 └───────────┘             
src                  └───────────┘                
typ                └───────────┘             
261  have set.prod u v ⊆ n, from assume ⟨x',y'⟩ ⟨hx',hy'⟩,
id        └──────┘                  └┘         └─┘
src       └──────┘     
typ       └──────┘                  └┘         └─┘
doc       └──────┘
262    have ∃i ∈ s0, x' ∈ (uvs i).1, by simpa using hx',
id                                            └─┘
src                                 └──────────┘
typ                               └──────────┘└─┘
doc                                     └──────────┘
txt                                     └──────────┘
par                                     └──────────┘
pid                                          └────┘
st                                     └──────────────┘
263    let ⟨i,is0,hi⟩ := this in
id     └─┘   └─┘ └┘     └──┘
typ    └─┘   └─┘ └┘     └──┘
264    (h i).2.2.2.2 ⟨hi, (bInter_subset_of_mem is0 : v ⊆ (uvs i).2) hy'⟩,
id                     └──────────────────┘                
src                    └──────────────────┘                 
typ                    └──────────────────┘                
265  ⟨u, v, ‹is_open u›, ‹is_open v›, s0_cover, ‹t ⊆ v›, ‹set.prod u v ⊆ n›⟩
id        └─────┘   └─────┘                 └──────┘    
src         └─────┘    └─────┘                    └──────┘       
typ       └─────┘   └─────┘                 └──────┘    
doc         └─────┘    └─────┘                     └──────┘        
266  
267  lemma generalized_tube_lemma {s : set α} (hs : compact s) {t : set β} (ht : compact t)
id                                     └─┘         └─────┘        └─┘         └─────┘ 
src                                    └─┘          └─────┘         └─┘          └─────┘
typ                                    └─┘         └─────┘        └─┘         └─────┘ 
doc                                                 └─────┘                      └─────┘
268    {n : set (α × β)} (hn : is_open n) (hp : set.prod s t ⊆ n) :
id          └─┘             └─────┘         └──────┘    
src         └─┘               └─────┘          └──────┘     
typ         └─┘             └─────┘         └──────┘    
doc                            └─────┘          └──────┘
269    ∃ (u : set α) (v : set β), is_open u ∧ is_open v ∧ s ⊆ u ∧ t ⊆ v ∧ set.prod u v ⊆ n :=
id           └─┘        └─┘   └─────┘   └─────┘           └──────┘    
src          └─┘         └─┘    └─────┘    └─────┘                └──────┘     
typ          └─┘        └─┘   └─────┘   └─────┘           └──────┘    
doc                               └─────┘     └─────┘                     └──────┘
270  have _, from
271    nhds_contain_boxes_of_compact hs t $ assume x _, nhds_contain_boxes.symm $
id     └───────────────────────────┘ └┘              └─────────────────────┘
src    └───────────────────────────┘                    └─────────────────────┘
typ    └───────────────────────────┘ └┘              └─────────────────────┘
272      nhds_contain_boxes_of_compact ht {x} $ assume y _, nhds_contain_boxes_of_singleton,
id       └───────────────────────────┘ └┘               └─────────────────────────────┘
src      └───────────────────────────┘                     └─────────────────────────────┘
typ      └───────────────────────────┘ └┘               └─────────────────────────────┘
273  this n hn hp
id   └──┘  └┘ └┘
typ  └──┘  └┘ └┘
274  
275  end tube_lemma
276  
277  /-- Type class for compact spaces. Separation is sometimes included in the definition, especially
278  in the French literature, but we do not include it here. -/
279  class compact_space (α : Type*) [topological_space α] : Prop :=
id                            └───┘   └───────────────┘ 
src                                   └───────────────┘
typ                           └───┘   └───────────────┘ 
doc                                   └───────────────┘
280  (compact_univ : compact (univ : set α))
id                   └─────┘  └──┘   └─┘ 
src                  └─────┘  └──┘   └─┘
typ                  └─────┘  └──┘   └─┘ 
doc                  └─────┘
281  
282  lemma compact_univ [h : compact_space α] : compact (univ : set α) := h.compact_univ
id                           └───────────┘     └─────┘  └──┘   └─┘      └───────────┘
src                          └───────────┘      └─────┘  └──┘   └─┘        └───────────┘
typ                          └───────────┘     └─────┘  └──┘   └─┘      └───────────┘
doc                          └───────────┘      └─────┘
283  
284  lemma is_closed.compact [compact_space α] {s : set α} (h : is_closed s) :
id                            └───────────┘        └─┘        └───────┘ 
src                           └───────────┘         └─┘         └───────┘
typ                           └───────────┘        └─┘        └───────┘ 
doc                           └───────────┘                     └───────┘
285    compact s :=
id     └─────┘ 
src    └─────┘
typ    └─────┘ 
doc    └─────┘
286  compact_of_is_closed_subset compact_univ h (subset_univ _)
id   └─────────────────────────┘ └──────────┘   └─────────┘
src  └─────────────────────────┘ └──────────┘    └─────────┘
typ  └─────────────────────────┘ └──────────┘   └─────────┘
287  
288  variables [topological_space β]
id              └───────────────┘
src             └───────────────┘
typ             └───────────────┘
doc             └───────────────┘
289  
290  lemma compact.image_of_continuous_on {s : set α} {f : α → β} (hs : compact s)
id                                             └─┘                   └─────┘ 
src                                            └─┘                      └─────┘
typ                                            └─┘                   └─────┘ 
doc                                                                     └─────┘
291    (hf : continuous_on f s) : compact (f '' s) :=
id           └───────────┘      └─────┘   └┘ 
src          └───────────┘        └─────┘    └┘
typ          └───────────┘      └─────┘   └┘ 
doc          └───────────┘        └─────┘
292  begin
st   └─────
293    intros l lne ls,
src    └─────────────┘
typ    └─────────────┘
doc    └─────────────┘
txt    └─────────────┘
par    └─────────────┘
pid          └───────┘
st   ────────────────┘└─
294    have ne_bot : l.comap f ⊓ principal s ≠ ⊥,
id                   └─────┘   └───────┘   
src    └────────────┘└─────┘ └───────┘ 
typ    └────────────┘└─────┘└───────┘
doc    └────────────┘└─────┘  └───────┘  
txt    └────────────┘                    
par    └────────────┘                    
pid    └─────────┘└─┘                    
st   ──────────────────────────────────────────┘└─
295      from comap_inf_principal_ne_bot_of_image_mem lne (le_principal_iff.1 ls),
id            └─────────────────────────────────────┘ └─┘  └──────────────┘   └┘
src      └───┘└─────────────────────────────────────┘    └──────────────┘└─┘  
typ      └───┘└─────────────────────────────────────┘└─┘ └──────────────┘└─┘└┘
doc      └───┘                                                           └─┘  
txt      └───┘                                                           └─┘  
par      └───┘                                                           └─┘  
pid      └───┘                                                           └─┘  
st   ───────────────────────────────────────────────────────────────────────────┘└─
296    rcases hs (l.comap f ⊓ principal s) ne_bot inf_le_right with ⟨a, has, ha⟩,
id            └┘  └─────┘    └───────┘   └────┘ └──────────┘
src    └─────┘   └─────┘  └───────┘ └┘      └──────────┘└────────────────┘
typ    └─────┘└┘ └─────┘ └───────┘└┘└────┘└──────────┘└────────────────┘
doc    └─────┘   └─────┘  └───────┘ └┘                  └────────────────┘
txt    └─────┘                      └┘                  └────────────────┘
par    └─────┘                      └┘                  └────────────────┘
pid                                └┘                  └────────────────┘
st   ──────────────────────────────────────────────────────────────────────────┘└─
297    use [f a, mem_image_of_mem f has],
id             └──────────────┘  └─┘
src    └───┘  └┘└──────────────┘    
typ    └───┘└┘└──────────────┘└─┘
doc    └───┘  └┘                    
txt    └───┘  └┘                    
par    └───┘  └┘                    
pid       └┘  └┘                    
st   ──────────────────────────────────┘└─
298    rw [inf_assoc, @inf_comm _ _ _ (𝓝 a)] at ha,
id         └───────┘   └──────┘         
src    └──┘└───────┘└┘ └──────┘└─────┘  └──────┘
typ    └──┘└───────┘└┘ └──────┘└─────┘ └──────┘
doc    └──┘         └┘         └─────┘  └──────┘
txt    └──┘         └┘         └─────┘   └──────┘
par    └──┘         └┘         └─────┘   └──────┘
pid      └┘         └┘         └─────┘   └┘└────┘
st   ──────────────┘└─────────────────────┘└────┘└─
299    exact ne_bot_of_le_ne_bot (@@map_ne_bot f ha) (tendsto_comap.inf $ hf a has)
id           └─────────────────┘    └────────┘  └┘   └───────────────┘   └┘  └─┘
src    └────┘└─────────────────┘   └────────┘   └┘ └───────────────┘       └┘
typ    └────┘└─────────────────┘   └────────┘└┘└┘ └───────────────┘ └┘└─┘└┘
doc    └────┘                                   └┘                         └┘
txt    └────┘                                   └┘                         └┘
par    └────┘                                   └┘                         └┘
pid                                            └┘                         
st   ──────────────────────────────────────────────────────────────────────────────┘
300  end
st   └─┘
301  
302  lemma compact.image {s : set α} {f : α → β} (hs : compact s) (hf : continuous f) :
id                            └─┘                   └─────┘         └────────┘ 
src                           └─┘                      └─────┘          └────────┘
typ                           └─┘                   └─────┘         └────────┘ 
doc                                                    └─────┘          └────────┘
303    compact (f '' s) :=
id     └─────┘   └┘ 
src    └─────┘    └┘
typ    └─────┘   └┘ 
doc    └─────┘
304  hs.image_of_continuous_on hf.continuous_on
id   └┘└─────────────────────┘ └┘└────────────┘
src    └─────────────────────┘   └────────────┘
typ  └┘└─────────────────────┘ └┘└────────────┘
305  
306  lemma compact_range [compact_space α] {f : α → β} (hf : continuous f) :
id                        └───────────┘                   └────────┘ 
src                       └───────────┘                      └────────┘
typ                       └───────────┘                   └────────┘ 
doc                       └───────────┘                      └────────┘
307    compact (range f) :=
id     └─────┘  └───┘ 
src    └─────┘  └───┘
typ    └─────┘  └───┘ 
doc    └─────┘  └───┘
308  by rw ← image_univ; exact compact_univ.image hf
id           └────────┘        └────────────────┘ └┘
src     └───┘└────────┘  └────┘└────────────────┘  
typ     └───┘└────────┘  └────┘└────────────────┘└┘
doc     └───┘            └────┘                    
txt     └───┘            └────┘                    
par     └───┘            └────┘                    
pid       └─┘                                     
st     └─────────────────────────────────────────────
309  
src  
typ  
doc  
txt  
par  
pid  
st   
310  lemma embedding.compact_iff_compact_image {s : set α} {f : α → β} (hf : embedding f) :
id                                                  └─┘                   └───────┘ 
src                                                 └─┘                      └───────┘
typ                                                 └─┘                   └───────┘ 
doc                                                                          └───────┘
311    compact s ↔ compact (f '' s) :=
id     └─────┘   └─────┘   └┘ 
src    └─────┘    └─────┘    └┘
typ    └─────┘   └─────┘   └┘ 
doc    └─────┘     └─────┘
312  iff.intro (assume h, h.image hf.continuous) $ assume h, begin
id   └───────┘           └────┘ └┘└─────────┘           
src  └───────┘             └────┘   └─────────┘
typ  └───────┘           └────┘ └┘└─────────┘           
st                                                           └─────
313    rw compact_iff_ultrafilter_le_nhds at ⊢ h,
id        └─────────────────────────────┘
src    └─┘└─────────────────────────────┘└─────┘
typ    └─┘└─────────────────────────────┘└─────┘
doc    └─┘                               └─────┘
txt    └─┘                               └─────┘
par    └─┘                               └─────┘
pid                                     └─────┘
st   ──────────────────────────────────────────┘└─
314    intros u hu us',
src    └─────────────┘
typ    └─────────────┘
doc    └─────────────┘
txt    └─────────────┘
par    └─────────────┘
pid          └───────┘
st   ────────────────┘└─
315    let u' : filter β := map f u,
id              └────┘     └─┘  
src    └───────┘└────┘ └──┘└─┘ 
typ    └───────┘└────┘└──┘└─┘
doc    └───────┘       └──┘└─┘ 
txt    └───────┘       └──┘    
par    └───────┘       └──┘    
pid    └────┘└─┘       └──┘    
st   ─────────────────────────────┘└─
316    have : u' ≤ principal (f '' s), begin
id            └┘  └───────┘   └┘ 
src    └─────┘  └───────┘  └┘ 
typ    └─────┘└┘└───────┘ └┘
doc    └─────┘   └───────┘     
txt    └─────┘                 
par    └─────┘                 
pid    └───┘└┘                 
st   ───────────────────────────────┘└─────┘
317      rw [map_le_iff_le_comap, comap_principal], convert us',
id           └─────────────────┘  └─────────────┘           └─┘
src      └──┘└─────────────────┘└┘└─────────────┘  └──────┘
typ      └──┘└─────────────────┘└┘└─────────────┘  └──────┘└─┘
doc      └──┘                   └┘                 └──────┘
txt      └──┘                   └┘                 └──────┘
par      └──┘                   └┘                 └──────┘
pid        └┘                   └┘                        
st   ──────────────────────────┘└───────────────┘└────────────┘└─
318      exact preimage_image_eq _ hf.inj
id             └───────────────┘   └────┘
src      └────┘└───────────────┘└─┘└────┘
typ      └────┘└───────────────┘└─┘└────┘
doc      └────┘                 └─┘      
txt      └────┘                 └─┘      
par      └────┘                 └─┘      
pid                            └─┘      
st   ─────────────────────────────────────
319    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘└─
320    rcases h u' (ultrafilter_map hu) this with ⟨_, ⟨a, ha, ⟨⟩⟩, _⟩,
id             └┘  └─────────────┘ └┘  └──┘
src    └─────┘    └─────────────┘  └┘    └───────────────────────┘
typ    └─────┘└┘ └─────────────┘└┘└┘└──┘└───────────────────────┘
doc    └─────┘                     └┘    └───────────────────────┘
txt    └─────┘                     └┘    └───────────────────────┘
par    └─────┘                     └┘    └───────────────────────┘
pid                               └┘    └───────────────────────┘
st   ───────────────────────────────────────────────────────────────┘└─
321    refine ⟨a, ha, _⟩,
id               └┘
src    └─────┘  └┘  └──┘
typ    └─────┘ └┘└┘└──┘
doc    └─────┘  └┘  └──┘
txt    └─────┘  └┘  └──┘
par    └─────┘  └┘  └──┘
pid            └┘  └──┘
st   ──────────────────┘└─
322    rwa [hf.induced, nhds_induced, ←map_le_iff_le_comap]
id                      └──────────┘   └─────────────────┘
src    └───┘          └┘└──────────┘└─┘└─────────────────┘└┘
typ    └───┘└────────┘└┘└──────────┘└─┘└─────────────────┘└┘
doc    └───┘          └┘            └─┘                   └┘
txt    └───┘          └┘            └─┘                   └┘
par    └───┘          └┘            └─┘                   └┘
pid       └┘          └┘            └─┘                   
st   ────────────────┘└────────────┘└────────────────────┘
323  end
st   └─┘
324  
325  lemma compact_iff_compact_in_subtype {p : α → Prop} {s : set {a // p a}} :
id                                                           └─┘      
src                                                           └─┘ 
typ                                                          └─┘      
326    compact s ↔ compact (subtype.val '' s) :=
id     └─────┘   └─────┘  └─────────┘ └┘ 
src    └─────┘    └─────┘  └─────────┘ └┘
typ    └─────┘   └─────┘  └─────────┘ └┘ 
doc    └─────┘     └─────┘
327  embedding_subtype_val.compact_iff_compact_image
id   └───────────────────┘└────────────────────────┘
src  └───────────────────┘└────────────────────────┘
typ  └───────────────────┘└────────────────────────┘
328  
329  lemma compact_iff_compact_univ {s : set α} : compact s ↔ compact (univ : set (subtype s)) :=
id                                       └─┘     └─────┘   └─────┘  └──┘   └─┘  └─────┘ 
src                                      └─┘      └─────┘    └─────┘  └──┘   └─┘  └─────┘
typ                                      └─┘     └─────┘   └─────┘  └──┘   └─┘  └─────┘ 
doc                                               └─────┘     └─────┘
330  by rw [compact_iff_compact_in_subtype, image_univ, subtype.val_range]; refl
id          └────────────────────────────┘  └────────┘  └───────────────┘
src     └──┘└────────────────────────────┘└┘└────────┘└┘└───────────────┘  └────
typ     └──┘└────────────────────────────┘└┘└────────┘└┘└───────────────┘  └────
doc     └──┘                              └┘          └┘                   └────
txt     └──┘                              └┘          └┘                   └────
par     └──┘                              └┘          └┘                   └────
pid       └┘                              └┘          └┘                       
st     └─────────────────────────────────┘└──────────┘└─────────────────┘└──────
331  
src  
typ  
doc  
txt  
par  
pid  
st   
332  lemma compact_iff_compact_space {s : set α} : compact s ↔ compact_space s :=
id                                        └─┘     └─────┘   └───────────┘ 
src                                       └─┘      └─────┘    └───────────┘
typ                                       └─┘     └─────┘   └───────────┘ 
doc                                                └─────┘     └───────────┘
333  compact_iff_compact_univ.trans ⟨λ h, ⟨h⟩, @compact_space.compact_univ _ _⟩
id   └──────────────────────┘└────┘           └────────────────────────┘
src  └──────────────────────┘└────┘             └────────────────────────┘
typ  └──────────────────────┘└────┘           └────────────────────────┘
334  
335  lemma compact.prod {s : set α} {t : set β} (hs : compact s) (ht : compact t) : compact (set.prod s t) :=
id                           └─┘        └─┘         └─────┘         └─────┘     └─────┘  └──────┘  
src                          └─┘         └─┘          └─────┘          └─────┘      └─────┘  └──────┘
typ                          └─┘        └─┘         └─────┘         └─────┘     └─────┘  └──────┘  
doc                                                   └─────┘          └─────┘      └─────┘  └──────┘
336  begin
st   └─────
337    rw compact_iff_ultrafilter_le_nhds at hs ht ⊢,
id        └─────────────────────────────┘
src    └─┘└─────────────────────────────┘└─────────┘
typ    └─┘└─────────────────────────────┘└─────────┘
doc    └─┘                               └─────────┘
txt    └─┘                               └─────────┘
par    └─┘                               └─────────┘
pid                                     └─────────┘
st   ──────────────────────────────────────────────┘└─
338    intros f hf hfs,
src    └─────────────┘
typ    └─────────────┘
doc    └─────────────┘
txt    └─────────────┘
par    └─────────────┘
pid          └───────┘
st   ────────────────┘└─
339    rw le_principal_iff at hfs,
id        └──────────────┘
src    └─┘└──────────────┘└─────┘
typ    └─┘└──────────────┘└─────┘
doc    └─┘                └─────┘
txt    └─┘                └─────┘
par    └─┘                └─────┘
pid                      └─────┘
st   ───────────────────────────┘└─
340    rcases hs (map prod.fst f) (ultrafilter_map hf)
id            └┘  └─┘ └──────┘    └─────────────┘ └┘
src    └─────┘   └─┘└──────┘ └┘ └─────────────┘  └─
typ    └─────┘└┘ └─┘└──────┘└┘ └─────────────┘└┘└─
doc    └─────┘   └─┘         └┘                  └─
txt    └─────┘               └┘                  └─
par    └─────┘               └┘                  └─
pid                         └┘                  └─
st   ──────────────────────────────────────────────────
341      (le_principal_iff.2 (mem_map_sets_iff.2
id        └──────────────┘    └──────────────┘
src  ───┘ └──────────────┘└─┘ └──────────────┘└──
typ  ───┘ └──────────────┘└─┘ └──────────────┘└──
doc  ───┘                 └─┘                 └──
txt  ───┘                 └─┘                 └──
par  ───┘                 └─┘                 └──
pid  ───┘                 └─┘                 └──
st   ────────────────────────────────────────────
342        ⟨_, hfs, image_subset_iff.2 (λ s h, h.1)⟩)) with ⟨a, sa, ha⟩,
id             └─┘  └──────────────┘
src  ─────┘ └─┘   └┘└──────────────┘└─┘  └────┘ └─────────────────────┘
typ  ─────┘ └─┘└─┘└┘└──────────────┘└─┘  └────┘ └─────────────────────┘
doc  ─────┘ └─┘   └┘└──────────────┘└─┘  └────┘ └─────────────────────┘
txt  ─────┘ └─┘   └┘                └─┘  └────┘ └─────────────────────┘
par  ─────┘ └─┘   └┘                └─┘  └────┘ └─────────────────────┘
pid  ─────┘ └─┘   └┘                └─┘  └────┘ └─────────────────────┘
st   ─────────────────────────────────────────────────────────────────┘└─
343    rcases ht (map prod.snd f) (ultrafilter_map hf)
id            └┘  └─┘ └──────┘    └─────────────┘ └┘
src    └─────┘   └─┘└──────┘ └┘ └─────────────┘  └─
typ    └─────┘└┘ └─┘└──────┘└┘ └─────────────┘└┘└─
doc    └─────┘   └─┘         └┘                  └─
txt    └─────┘               └┘                  └─
par    └─────┘               └┘                  └─
pid                         └┘                  └─
st   ──────────────────────────────────────────────────
344      (le_principal_iff.2 (mem_map_sets_iff.2
id        └──────────────┘    └──────────────┘
src  ───┘ └──────────────┘└─┘ └──────────────┘└──
typ  ───┘ └──────────────┘└─┘ └──────────────┘└──
doc  ───┘                 └─┘                 └──
txt  ───┘                 └─┘                 └──
par  ───┘                 └─┘                 └──
pid  ───┘                 └─┘                 └──
st   ────────────────────────────────────────────
345        ⟨_, hfs, image_subset_iff.2 (λ s h, h.2)⟩)) with ⟨b, tb, hb⟩,
id             └─┘  └──────────────┘
src  ─────┘ └─┘   └┘└──────────────┘└─┘  └────┘ └─────────────────────┘
typ  ─────┘ └─┘└─┘└┘└──────────────┘└─┘  └────┘ └─────────────────────┘
doc  ─────┘ └─┘   └┘└──────────────┘└─┘  └────┘ └─────────────────────┘
txt  ─────┘ └─┘   └┘                └─┘  └────┘ └─────────────────────┘
par  ─────┘ └─┘   └┘                └─┘  └────┘ └─────────────────────┘
pid  ─────┘ └─┘   └┘                └─┘  └────┘ └─────────────────────┘
st   ─────────────────────────────────────────────────────────────────┘└─
346    rw map_le_iff_le_comap at ha hb,
id        └─────────────────┘
src    └─┘└─────────────────┘└───────┘
typ    └─┘└─────────────────┘└───────┘
doc    └─┘                   └───────┘
txt    └─┘                   └───────┘
par    └─┘                   └───────┘
pid                         └───────┘
st   ────────────────────────────────┘└─
347    refine ⟨⟨a, b⟩, ⟨sa, tb⟩, _⟩,
id                    └┘  └┘
src    └─────┘   └┘ └─┘   └┘  └───┘
typ    └─────┘  └┘└─┘ └┘└┘└┘└───┘
doc    └─────┘   └┘ └─┘   └┘  └───┘
txt    └─────┘   └┘ └─┘   └┘  └───┘
par    └─────┘   └┘ └─┘   └┘  └───┘
pid             └┘ └─┘   └┘  └───┘
st   ─────────────────────────────┘└─
348    rw nhds_prod_eq, exact le_inf ha hb
id        └──────────┘        └────┘ └┘ └┘
src    └─┘└──────────┘  └────┘└────┘    
typ    └─┘└──────────┘  └────┘└────┘└┘└┘
doc    └─┘              └────┘          
txt    └─┘              └────┘          
par    └─┘              └────┘          
pid                                   
st   ────────────────┘└───────────────────┘
349  end
st   └─┘
350  
351  /-- Finite topological spaces are compact. -/
352  @[priority 100] instance fintype.compact_space [fintype α] : compact_space α :=
id                                                   └─────┘     └───────────┘ 
src                                                  └─────┘      └───────────┘
typ                                                  └─────┘     └───────────┘ 
doc                                                  └─────┘      └───────────┘
353  { compact_univ := set.finite_univ.compact }
id                     └─────────────┘└──────┘
src                    └─────────────┘└──────┘
typ                    └─────────────┘└──────┘
354  
355  /-- The product of two compact spaces is compact. -/
356  instance [compact_space α] [compact_space β] : compact_space (α × β) :=
id             └───────────┘    └───────────┘     └───────────┘    
src            └───────────┘     └───────────┘      └───────────┘    
typ            └───────────┘    └───────────┘     └───────────┘    
doc            └───────────┘     └───────────┘      └───────────┘
357  ⟨by { rw ← univ_prod_univ, exact compact_univ.prod compact_univ }⟩
id              └────────────┘        └───────────────┘ └──────────┘
src        └───┘└────────────┘  └────┘└───────────────┘└──────────┘
typ        └───┘└────────────┘  └────┘└───────────────┘└──────────┘
doc        └───┘                └────┘                             
txt        └───┘                └────┘                             
par        └───┘                └────┘                             
pid          └─┘                                                  
st      └────────────────────┘└─────────────────────────────────────┘└┘
358  
359  /-- The disjoint union of two compact spaces is compact. -/
360  instance [compact_space α] [compact_space β] : compact_space (α ⊕ β) :=
id             └───────────┘    └───────────┘     └───────────┘    
src            └───────────┘     └───────────┘      └───────────┘    
typ            └───────────┘    └───────────┘     └───────────┘    
doc            └───────────┘     └───────────┘      └───────────┘
361  ⟨begin
st    └─────
362    rw ← range_inl_union_range_inr,
id          └───────────────────────┘
src    └───┘└───────────────────────┘
typ    └───┘└───────────────────────┘
doc    └───┘
txt    └───┘
par    └───┘
pid      └─┘
st   ───────────────────────────────┘└─
363    exact (compact_range continuous_inl).union (compact_range continuous_inr)
id                          └────────────┘         └───────────┘ └────────────┘
src    └────┘              └────────────┘└──────┘ └───────────┘└────────────┘└┘
typ    └────┘              └────────────┘└──────┘ └───────────┘└────────────┘└┘
doc    └────┘                            └──────┘                            └┘
txt    └────┘                            └──────┘                            └┘
par    └────┘                            └──────┘                            └┘
pid                                     └──────┘                            
st   ───────────────────────────────────────────────────────────────────────────┘
364  end⟩
st   └─┘
365  
366  section tychonoff
367  variables {ι : Type*} {π : ι → Type*} [∀i, topological_space (π i)]
id                                            └───────────────┘    
src                                             └───────────────┘
typ                                           └───────────────┘    
doc                                             └───────────────┘
368  
369  /-- Tychonoff's theorem -/
370  lemma compact_pi_infinite {s : Πi:ι, set (π i)} :
id                                       └─┘   
src                                       └─┘
typ                                      └─┘   
371    (∀i, compact (s i)) → compact {x : Πi:ι, π i | ∀i, x i ∈ s i} :=
id         └─────┘        └─────┘                    
src         └─────┘          └─────┘                         
typ        └─────┘        └─────┘                    
doc         └─────┘          └─────┘
372  begin
st   └─────
373    simp [compact_iff_ultrafilter_le_nhds, nhds_pi],
id           └─────────────────────────────┘  └─────┘
src    └────┘└─────────────────────────────┘└┘└─────┘
typ    └────┘└─────────────────────────────┘└┘└─────┘
doc    └────┘                               └┘       
txt    └────┘                               └┘       
par    └────┘                               └┘       
pid                                       └┘       
st   ────────────────────────────────────────────────┘└─
374    exact assume h f hf hfs,
src    └────┘      └────────────
typ    └────┘      └────────────
doc    └────┘      └────────────
txt    └────┘      └────────────
par    └────┘      └────────────
pid               └────────────
st   ───────────────────────────
375      let p : Πi:ι, filter (π i) := λi, map (λx:Πi:ι, π i, x i) f in
id                     └────┘              └─┘
src  ───┘   └───┘ └┘  └────┘   └───┘ └─┘└─┘  └┘ └┘    └┘  └┘ └───
typ  ───┘   └───┘ └┘  └────┘   └───┘ └─┘└─┘  └┘ └┘    └┘  └┘ └───
doc  ───┘   └───┘ └┘           └───┘ └─┘└─┘  └┘ └┘    └┘  └┘ └───
txt  ───┘   └───┘ └┘           └───┘ └─┘     └┘ └┘    └┘  └┘ └───
par  ───┘   └───┘ └┘           └───┘ └─┘     └┘ └┘    └┘  └┘ └───
pid  ───┘   └───┘ └┘           └───┘ └─┘     └┘ └┘    └┘  └┘ └───
st   ───────────────────────────────────────────────────────────────────
376      have ∀i:ι, ∃a, a∈s i ∧ p i ≤ 𝓝 a,
id                                
src  ───┘     └┘         └─
typ  ───┘     └┘         └─
doc  ───┘     └┘             └─
txt  ───┘     └┘              └─
par  ───┘     └┘              └─
pid  ───┘     └┘              └─
st   ──────────────────────────────────────
377        from assume i, h i (p i) (ultrafilter_map hf) $
id                                   └─────────────┘
src  ──────────┘      └──┘     └┘ └─────────────┘  └┘ 
typ  ──────────┘      └──┘     └┘ └─────────────┘  └┘ 
doc  ──────────┘      └──┘     └┘                  └┘ 
txt  ──────────┘      └──┘     └┘                  └┘ 
par  ──────────┘      └──┘     └┘                  └┘ 
pid  ──────────┘      └──┘     └┘                  └┘ 
st   ──────────────────────────────────────────────────────
378        show (λx:Πi:ι, π i, x i) ⁻¹' s i ∈ f.sets,
id                                └─┘       └───┘
src  ─────┘      └┘ └┘    └┘  └┘└─┘    └───┘└─
typ  ─────┘      └┘ └┘  └┘  └┘└─┘   └───┘└─
doc  ─────┘      └┘ └┘    └┘  └┘└─┘         └─
txt  ─────┘      └┘ └┘    └┘  └┘            └─
par  ─────┘      └┘ └┘    └┘  └┘            └─
pid  ─────┘      └┘ └┘    └┘  └┘            └─
st   ─────────────────────────────────────────────────
379          from mem_sets_of_superset hfs $ assume x (hx : ∀i, x i ∈ s i), hx i,
id                └──────────────────┘                                
src  ────────────┘└──────────────────┘          └───────┘       └─┘   └─
typ  ────────────┘└──────────────────┘          └───────┘      └─┘   └─
doc  ────────────┘                              └───────┘       └─┘   └─
txt  ────────────┘                              └───────┘       └─┘   └─
par  ────────────┘                              └───────┘       └─┘   └─
pid  ────────────┘                              └───────┘       └─┘   └─
st   ─────────────────────────────────────────────────────────────────────────────
380      let ⟨a, ha⟩ := classical.axiom_of_choice this in
id              └┘     └───────────────────────┘
src  ───┘     └┘  └───┘└───────────────────────┘    └───
typ  ───┘    └┘└┘└───┘└───────────────────────┘    └───
doc  ───┘     └┘  └───┘                             └───
txt  ───┘     └┘  └───┘                             └───
par  ───┘     └┘  └───┘                             └───
pid  ───┘     └┘  └───┘                             └───
st   ─────────────────────────────────────────────────────
381      ⟨a, assume i, (ha i).left, assume i, map_le_iff_le_comap.mp $ (ha i).right⟩
id                                            └────────────────────┘
src  ───┘  └┘      └──┘    └──────┘      └──┘└────────────────────┘     └───────┘
typ  ───┘  └┘      └──┘    └──────┘      └──┘└────────────────────┘     └───────┘
doc  ───┘  └┘      └──┘    └──────┘      └──┘                           └───────┘
txt  ───┘  └┘      └──┘    └──────┘      └──┘                           └───────┘
par  ───┘  └┘      └──┘    └──────┘      └──┘                           └───────┘
pid  ───┘  └┘      └──┘    └──────┘      └──┘                           └──────┘
st   ───────────────────────────────────────────────────────────────────────────────┘
382  end
st   └─┘
383  
384  instance pi.compact [∀i:ι, compact_space (π i)] : compact_space (Πi, π i) :=
id                             └───────────┘        └───────────┘      
src                             └───────────┘          └───────────┘
typ                            └───────────┘        └───────────┘      
doc                             └───────────┘          └───────────┘
385  ⟨begin
st    └─────
386    have A : compact {x : Πi:ι, π i | ∀i, x i ∈ (univ : set (π i))} :=
id              └─────┘                          └──┘   └─┘  
src    └───────┘└─────┘└──┘ └┘    └─┘     └──┘└─┘└─┘   └──────
typ    └───────┘└─────┘└──┘ └┘   └─┘     └──┘└─┘└─┘  └──────
doc    └───────┘└─────┘ └──┘ └┘    └─┘          └─┘      └──────
txt    └───────┘        └──┘ └┘    └─┘          └─┘      └──────
par    └───────┘        └──┘ └┘    └─┘          └─┘      └──────
pid    └────┘└─┘        └──┘ └┘    └─┘          └─┘      └─┘└───
st   ─────────────────────────────────────────────────────────────────────
387      compact_pi_infinite (λi, compact_univ),
id       └─────────────────┘      └──────────┘
src  ───┘└─────────────────┘  └─┘└──────────┘
typ  ───┘└─────────────────┘  └─┘└──────────┘
doc  ───┘└─────────────────┘  └─┘            
txt  ───┘                     └─┘            
par  ───┘                     └─┘            
pid  ───┘                     └─┘            
st   ─────────────────────────────────────────┘└─
388    have : {x : Πi:ι, π i | ∀i, x i ∈ (univ : set (π i))} = univ := by ext; simp,
id                                             └─┘         └──┘
src    └─────┘└──┘ └┘    └─┘          └─┘└─┘   └──┘└──┘└──┘  └─┘└┘└──┘
typ    └─────┘└──┘ └┘   └─┘          └─┘└─┘  └──┘└──┘└──┘  └─┘└┘└──┘
doc    └─────┘ └──┘ └┘    └─┘          └─┘      └──┘     └──┘  └─┘└┘└──┘
txt    └─────┘ └──┘ └┘    └─┘          └─┘      └──┘     └──┘  └─┘└┘└──┘
par    └─────┘ └──┘ └┘    └─┘          └─┘      └──┘     └──┘  └─┘└┘└──┘
pid    └───┘└┘ └──┘ └┘    └─┘          └─┘      └──┘     └──┘  └────────┘
st   ───────────────────────────────────────────────────────────────────┘└────────┘└─
389    rwa this at A,
id         └──┘
src    └──┘    └───┘
typ    └──┘└──┘└───┘
doc    └──┘    └───┘
txt    └──┘    └───┘
par    └──┘    └───┘
pid           └───┘
st   ──────────────┘└─
390  end⟩
st   ──┘
391  
392  end tychonoff
393  
394  instance quot.compact_space {r : α → α → Prop} [compact_space α] :
id                                                 └───────────┘ 
src                                                  └───────────┘
typ                                                └───────────┘ 
doc                                                  └───────────┘
395    compact_space (quot r) :=
id     └───────────┘  └──┘ 
src    └───────────┘
typ    └───────────┘  └──┘ 
doc    └───────────┘
396  ⟨by { rw ← range_quot_mk, exact compact_range continuous_quot_mk }⟩
id              └───────────┘        └───────────┘ └────────────────┘
src        └───┘└───────────┘  └────┘└───────────┘└────────────────┘
typ        └───┘└───────────┘  └────┘└───────────┘└────────────────┘
doc        └───┘               └────┘                               
txt        └───┘               └────┘                               
par        └───┘               └────┘                               
pid          └─┘                                                   
st      └───────────────────┘└───────────────────────────────────────┘└┘
397  
398  instance quotient.compact_space {s : setoid α} [compact_space α] :
id                                        └────┘    └───────────┘ 
src                                       └────┘     └───────────┘
typ                                       └────┘    └───────────┘ 
doc                                                  └───────────┘
399    compact_space (quotient s) :=
id     └───────────┘  └──────┘ 
src    └───────────┘  └──────┘
typ    └───────────┘  └──────┘ 
doc    └───────────┘
400  quot.compact_space
id   └────────────────┘
src  └────────────────┘
typ  └────────────────┘
401  
402  /-- There are various definitions of "locally compact space" in the literature, which agree for
403  Hausdorff spaces but not in general. This one is the precise condition on X needed for the
404  evaluation `map C(X, Y) × X → Y` to be continuous for all `Y` when `C(X, Y)` is given the
405  compact-open topology. -/
406  class locally_compact_space (α : Type*) [topological_space α] : Prop :=
id                                    └───┘   └───────────────┘ 
src                                           └───────────────┘
typ                                   └───┘   └───────────────┘ 
doc                                           └───────────────┘
407  (local_compact_nhds : ∀ (x : α) (n ∈ 𝓝 x), ∃ s ∈ 𝓝 x, s ⊆ n ∧ compact s)
id                                                   └─────┘ 
src                                                          └─────┘
typ                                                  └─────┘ 
doc                                                              └─────┘
408  
409  end compact
410  
411  section clopen
412  
413  /-- A set is clopen if it is both open and closed. -/
414  def is_clopen (s : set α) : Prop :=
id                      └─┘ 
src                     └─┘
typ                     └─┘ 
415  is_open s ∧ is_closed s
id   └─────┘   └───────┘ 
src  └─────┘    └───────┘
typ  └─────┘   └───────┘ 
doc  └─────┘     └───────┘
416  
417  theorem is_clopen_union {s t : set α} (hs : is_clopen s) (ht : is_clopen t) : is_clopen (s ∪ t) :=
id                                  └─┘         └───────┘         └───────┘     └───────┘    
src                                 └─┘          └───────┘          └───────┘      └───────┘    
typ                                 └─┘         └───────┘         └───────┘     └───────┘    
doc                                              └───────┘          └───────┘      └───────┘
418  ⟨is_open_union hs.1 ht.1, is_closed_union hs.2 ht.2⟩
id    └───────────┘ └┘  └┘   └─────────────┘ └┘  └┘
src   └───────────┘          └─────────────┘       
typ   └───────────┘ └┘  └┘   └─────────────┘ └┘  └┘
419  
420  theorem is_clopen_inter {s t : set α} (hs : is_clopen s) (ht : is_clopen t) : is_clopen (s ∩ t) :=
id                                  └─┘         └───────┘         └───────┘     └───────┘    
src                                 └─┘          └───────┘          └───────┘      └───────┘    
typ                                 └─┘         └───────┘         └───────┘     └───────┘    
doc                                              └───────┘          └───────┘      └───────┘
421  ⟨is_open_inter hs.1 ht.1, is_closed_inter hs.2 ht.2⟩
id    └───────────┘ └┘  └┘   └─────────────┘ └┘  └┘
src   └───────────┘          └─────────────┘       
typ   └───────────┘ └┘  └┘   └─────────────┘ └┘  └┘
422  
423  @[simp] theorem is_clopen_empty : is_clopen (∅ : set α) :=
id                                     └───────┘     └─┘ 
src                                    └───────┘     └─┘
typ                                    └───────┘     └─┘ 
doc    └──┘                            └───────┘
424  ⟨is_open_empty, is_closed_empty⟩
id    └───────────┘  └─────────────┘
src   └───────────┘  └─────────────┘
typ   └───────────┘  └─────────────┘
425  
426  @[simp] theorem is_clopen_univ : is_clopen (univ : set α) :=
id                                    └───────┘  └──┘   └─┘ 
src                                   └───────┘  └──┘   └─┘
typ                                   └───────┘  └──┘   └─┘ 
doc    └──┘                           └───────┘
427  ⟨is_open_univ, is_closed_univ⟩
id    └──────────┘  └────────────┘
src   └──────────┘  └────────────┘
typ   └──────────┘  └────────────┘
428  
429  theorem is_clopen_compl {s : set α} (hs : is_clopen s) : is_clopen (-s) :=
id                                └─┘         └───────┘     └───────┘  
src                               └─┘          └───────┘      └───────┘  
typ                               └─┘         └───────┘     └───────┘  
doc                                            └───────┘      └───────┘
430  ⟨hs.2, is_closed_compl_iff.2 hs.1⟩
id    └┘   └─────────────────┘  └┘
src        └─────────────────┘    
typ   └┘   └─────────────────┘  └┘
431  
432  @[simp] theorem is_clopen_compl_iff {s : set α} : is_clopen (-s) ↔ is_clopen s :=
id                                            └─┘     └───────┘     └───────┘ 
src                                           └─┘      └───────┘      └───────┘
typ                                           └─┘     └───────┘     └───────┘ 
doc    └──┘                                            └───────┘        └───────┘
433  ⟨λ h, compl_compl s ▸ is_clopen_compl h, is_clopen_compl⟩
id        └─────────┘   └─────────────┘   └─────────────┘
src        └─────────┘    └─────────────┘    └─────────────┘
typ       └─────────┘   └─────────────┘   └─────────────┘
434  
435  theorem is_clopen_diff {s t : set α} (hs : is_clopen s) (ht : is_clopen t) : is_clopen (s-t) :=
id                                 └─┘         └───────┘         └───────┘     └───────┘  
src                                └─┘          └───────┘          └───────┘      └───────┘   
typ                                └─┘         └───────┘         └───────┘     └───────┘  
doc                                             └───────┘          └───────┘      └───────┘
436  is_clopen_inter hs (is_clopen_compl ht)
id   └─────────────┘ └┘  └─────────────┘ └┘
src  └─────────────┘     └─────────────┘
typ  └─────────────┘ └┘  └─────────────┘ └┘
437  
438  end clopen
439  
440  section irreducible
441  
442  /-- An irreducible set is one where there is no non-trivial pair of disjoint opens. -/
443  def is_irreducible (s : set α) : Prop :=
id                           └─┘ 
src                          └─┘
typ                          └─┘ 
444  ∀ (u v : set α), is_open u → is_open v →
id            └─┘    └─────┘    └─────┘ 
src           └─┘     └─────┘     └─────┘
typ           └─┘    └─────┘    └─────┘ 
doc                   └─────┘     └─────┘
445    (∃ x, x ∈ s ∩ u) → (∃ x, x ∈ s ∩ v) → ∃ x, x ∈ s ∩ (u ∩ v)
id                                    
src                                              
typ                                   
446  
447  theorem is_irreducible_empty : is_irreducible (∅ : set α) :=
id                                  └────────────┘     └─┘ 
src                                 └────────────┘     └─┘
typ                                 └────────────┘     └─┘ 
doc                                 └────────────┘
448  λ _ _ _ _ _ ⟨x, h1, h2⟩, h1.elim
id             └┘         └───┘
src                             └───┘
typ            └┘         └───┘
449  
450  theorem is_irreducible_singleton {x} : is_irreducible ({x} : set α) :=
id                                          └────────────┘      └─┘ 
src                                         └────────────┘       └─┘
typ                                         └────────────┘      └─┘ 
doc                                         └────────────┘
451  λ u v _ _ ⟨y, h1, h2⟩ ⟨z, h3, h4⟩, by rw mem_singleton_iff at h1 h3;
id                                      └───────────────┘
src                                        └─┘└───────────────┘└───────┘
typ                                  └─┘└───────────────┘└───────┘
doc                                        └─┘                 └───────┘
txt                                        └─┘                 └───────┘
par                                        └─┘                 └───────┘
pid                                                           └───────┘
st                                        └───────────────────────────────
452  substs y z; exact ⟨x, or.inl rfl, h2, h4⟩
id                        └────┘ └─┘  └┘  └┘
src  └────────┘  └────┘  └┘└────┘└─┘└┘  └┘  └─
typ  └────────┘  └────┘ └┘└────┘└─┘└┘└┘└┘└┘└─
doc  └────────┘  └────┘  └┘         └┘  └┘  └─
txt  └────────┘  └────┘  └┘         └┘  └┘  └─
par  └────────┘  └────┘  └┘         └┘  └┘  └─
pid        └──┘         └┘         └┘  └┘  
st   ──────────────────────────────────────────
453  
src  
typ  
doc  
txt  
par  
pid  
st   
454  theorem is_irreducible_closure {s : set α} (H : is_irreducible s) :
id                                       └─┘        └────────────┘ 
src                                      └─┘         └────────────┘
typ                                      └─┘        └────────────┘ 
doc                                                  └────────────┘
455    is_irreducible (closure s) :=
id     └────────────┘  └─────┘ 
src    └────────────┘  └─────┘
typ    └────────────┘  └─────┘ 
doc    └────────────┘  └─────┘
456  λ u v hu hv ⟨y, hycs, hyu⟩ ⟨z, hzcs, hzv⟩,
id       └┘ └┘    └──┘  └─┘     └──┘  └─┘
typ      └┘ └┘    └──┘  └─┘     └──┘  └─┘
457  let ⟨p, hpu, hps⟩ := mem_closure_iff.1 hycs u hu hyu in
id   └─┘    └─┘  └─┘     └─────────────┘        └┘
src                       └─────────────┘
typ  └─┘    └─┘  └─┘     └─────────────┘        └┘
458  let ⟨q, hqv, hqs⟩ := mem_closure_iff.1 hzcs v hv hzv in
id   └─┘    └─┘  └─┘     └─────────────┘        └┘
src                       └─────────────┘
typ  └─┘    └─┘  └─┘     └─────────────┘        └┘
459  let ⟨r, hrs, hruv⟩ := H u v hu hv ⟨p, hps, hpu⟩ ⟨q, hqs, hqv⟩ in
id   └─┘    └─┘  └──┘        └┘ └┘
typ  └─┘    └─┘  └──┘        └┘ └┘
460  ⟨r, subset_closure hrs, hruv⟩
id       └────────────┘
src      └────────────┘
typ      └────────────┘
461  
462  theorem exists_irreducible (s : set α) (H : is_irreducible s) :
id                                   └─┘        └────────────┘ 
src                                  └─┘         └────────────┘
typ                                  └─┘        └────────────┘ 
doc                                              └────────────┘
463    ∃ t : set α, is_irreducible t ∧ s ⊆ t ∧ ∀ u, is_irreducible u → t ⊆ u → u = t :=
id          └─┘  └────────────┘           └────────────┘           
src         └─┘   └────────────┘               └────────────┘              
typ         └─┘  └────────────┘           └────────────┘           
doc                 └────────────┘                  └────────────┘
464  let ⟨m, hm, hsm, hmm⟩ := zorn.zorn_subset₀ { t : set α | is_irreducible t }
id   └─┘    └┘  └─┘  └─┘     └───────────────┘      └─┘    └────────────┘ 
src                           └───────────────┘      └─┘     └────────────┘
typ  └─┘    └┘  └─┘  └─┘     └───────────────┘      └─┘    └────────────┘ 
doc                                                           └────────────┘
465    (λ c hc hcc hcn, let ⟨t, htc⟩ := hcn in
id         └┘ └─┘ └─┘  └─┘             └─┘
typ        └┘ └─┘ └─┘  └─┘             └─┘
466      ⟨⋃₀ c, λ u v hu hv ⟨y, hy, hyu⟩ ⟨z, hz, hzv⟩,
id        └┘       └┘ └┘   └┘  └─┘    └┘  └─┘
src       └┘
typ       └┘       └┘ └┘   └┘  └─┘    └┘  └─┘
467        let ⟨p, hpc, hyp⟩ := mem_sUnion.1 hy,
id         └─┘    └─┘  └─┘     └────────┘
src                             └────────┘
typ        └─┘    └─┘  └─┘     └────────┘
468            ⟨q, hqc, hzq⟩ := mem_sUnion.1 hz in
id                └─┘  └─┘     └────────┘
src                             └────────┘
typ               └─┘  └─┘     └────────┘
469        or.cases_on (zorn.chain.total hcc hpc hqc)
id         └─────────┘  └──────────────┘ └─┘
src        └─────────┘  └──────────────┘
typ        └─────────┘  └──────────────┘ └─┘
470          (assume hpq : p ⊆ q, let ⟨x, hxp, hxuv⟩ := hc hqc u v hu hv
id                               └─┘    └─┘  └──┘     └┘       └┘ └┘
src                          
typ                              └─┘    └─┘  └──┘     └┘       └┘ └┘
471              ⟨y, hpq hyp, hyu⟩ ⟨z, hzq, hzv⟩ in
id                   └─┘
typ                  └─┘
472            ⟨x, mem_sUnion_of_mem hxp hqc, hxuv⟩)
id                 └───────────────┘
src                └───────────────┘
typ                └───────────────┘
473          (assume hqp : q ⊆ p, let ⟨x, hxp, hxuv⟩ := hc hpc u v hu hv
id                               └─┘    └─┘  └──┘     └┘       └┘ └┘
src                          
typ                              └─┘    └─┘  └──┘     └┘       └┘ └┘
474              ⟨y, hyp, hyu⟩ ⟨z, hqp hzq, hzv⟩ in
id                                 └─┘
typ                                └─┘
475            ⟨x, mem_sUnion_of_mem hxp hpc, hxuv⟩),
id                 └───────────────┘
src                └───────────────┘
typ                └───────────────┘
476      λ x hxc, set.subset_sUnion_of_mem hxc⟩) s H in
id          └─┘  └──────────────────────┘ └─┘    
src               └──────────────────────┘
typ         └─┘  └──────────────────────┘ └─┘    
477  ⟨m, hm, hsm, λ u hu hmu, hmm _ hu hmu⟩
id                   └┘ └─┘        └┘ └─┘
typ                  └┘ └─┘        └┘ └─┘
478  
479  /-- A maximal irreducible set that contains a given point. -/
480  def irreducible_component (x : α) : set α :=
id                                      └─┘ 
src                                      └─┘
typ                                     └─┘ 
481  classical.some (exists_irreducible {x} is_irreducible_singleton)
id   └────────────┘  └────────────────┘   └──────────────────────┘
src  └────────────┘  └────────────────┘    └──────────────────────┘
typ  └────────────┘  └────────────────┘   └──────────────────────┘
482  
483  theorem is_irreducible_irreducible_component {x : α} : is_irreducible (irreducible_component x) :=
id                                                         └────────────┘  └───────────────────┘ 
src                                                         └────────────┘  └───────────────────┘
typ                                                        └────────────┘  └───────────────────┘ 
doc                                                         └────────────┘  └───────────────────┘
484  (classical.some_spec (exists_irreducible {x} is_irreducible_singleton)).1
id    └─────────────────┘  └────────────────┘   └──────────────────────┘  
src   └─────────────────┘  └────────────────┘    └──────────────────────┘  
typ   └─────────────────┘  └────────────────┘   └──────────────────────┘  
485  
486  theorem mem_irreducible_component {x : α} : x ∈ irreducible_component x :=
id                                                └───────────────────┘ 
src                                                 └───────────────────┘
typ                                               └───────────────────┘ 
doc                                                  └───────────────────┘
487  singleton_subset_iff.1
id   └──────────────────┘
src  └──────────────────┘
typ  └──────────────────┘
488    (classical.some_spec (exists_irreducible {x} is_irreducible_singleton)).2.1
id      └─────────────────┘  └────────────────┘   └──────────────────────┘   
src     └─────────────────┘  └────────────────┘    └──────────────────────┘   
typ     └─────────────────┘  └────────────────┘   └──────────────────────┘   
489  
490  theorem eq_irreducible_component {x : α} :
id                                         
typ                                        
491    ∀ {s : set α}, is_irreducible s → irreducible_component x ⊆ s → s = irreducible_component x :=
id            └─┘    └────────────┘    └───────────────────┘        └───────────────────┘ 
src           └─┘     └────────────┘     └───────────────────┘           └───────────────────┘
typ           └─┘    └────────────┘    └───────────────────┘        └───────────────────┘ 
doc                   └────────────┘     └───────────────────┘             └───────────────────┘
492  (classical.some_spec (exists_irreducible {x} is_irreducible_singleton)).2.2
id    └─────────────────┘  └────────────────┘   └──────────────────────┘   
src   └─────────────────┘  └────────────────┘    └──────────────────────┘   
typ   └─────────────────┘  └────────────────┘   └──────────────────────┘   
493  
494  theorem is_closed_irreducible_component {x : α} :
id                                                
typ                                               
495    is_closed (irreducible_component x) :=
id     └───────┘  └───────────────────┘ 
src    └───────┘  └───────────────────┘
typ    └───────┘  └───────────────────┘ 
doc    └───────┘  └───────────────────┘
496  closure_eq_iff_is_closed.1 $ eq_irreducible_component
id   └──────────────────────┘    └──────────────────────┘
src  └──────────────────────┘    └──────────────────────┘
typ  └──────────────────────┘    └──────────────────────┘
497    (is_irreducible_closure is_irreducible_irreducible_component)
id      └────────────────────┘ └──────────────────────────────────┘
src     └────────────────────┘ └──────────────────────────────────┘
typ     └────────────────────┘ └──────────────────────────────────┘
498    subset_closure
id     └────────────┘
src    └────────────┘
typ    └────────────┘
499  
500  /-- An irreducible space is one where there is no non-trivial pair of disjoint opens. -/
501  class irreducible_space (α : Type u) [topological_space α] : Prop :=
id                                └──┘     └───────────────┘ 
src                                        └───────────────┘
typ                               └──┘     └───────────────┘ 
doc                                        └───────────────┘
502  (is_irreducible_univ : is_irreducible (univ : set α))
id                          └────────────┘  └──┘   └─┘ 
src                         └────────────┘  └──┘   └─┘
typ                         └────────────┘  └──┘   └─┘ 
doc                         └────────────┘
503  
504  theorem irreducible_exists_mem_inter [irreducible_space α] {s t : set α} :
id                                         └───────────────┘          └─┘ 
src                                        └───────────────┘           └─┘
typ                                        └───────────────┘          └─┘ 
doc                                        └───────────────┘
505    is_open s → is_open t → (∃ x, x ∈ s) → (∃ x, x ∈ t) → ∃ x, x ∈ s ∩ t :=
id     └─────┘    └─────┘                            
src    └─────┘     └─────┘                                     
typ    └─────┘    └─────┘                            
doc    └─────┘     └─────┘
506  by simpa only [univ_inter, univ_subset_iff] using
id                  └────────┘  └─────────────┘
src     └──────────┘└────────┘└┘└─────────────┘└───────
typ     └──────────┘└────────┘└┘└─────────────┘└───────
doc     └──────────┘          └┘               └───────
txt     └──────────┘          └┘               └───────
par     └──────────┘          └┘               └───────
pid          └──┘└┘          └┘               └─────
st     └───────────────────────────────────────────────
507    @irreducible_space.is_irreducible_univ α _ _ s t
id      └───────────────────────────────────┘       
src  ─┘ └───────────────────────────────────┘ └───┘  
typ  ─┘ └───────────────────────────────────┘└───┘
doc  ─┘                                       └───┘  
txt  ─┘                                       └───┘  
par  ─┘                                       └───┘  
pid  ─┘                                       └───┘  
st   ───────────────────────────────────────────────────
508  
src  
typ  
doc  
txt  
par  
pid  
st   
509  end irreducible
510  
511  section connected
512  
513  /-- A connected set is one where there is no non-trivial open partition. -/
514  def is_connected (s : set α) : Prop :=
id                         └─┘ 
src                        └─┘
typ                        └─┘ 
515  ∀ (u v : set α), is_open u → is_open v → s ⊆ u ∪ v →
id            └─┘    └─────┘    └─────┘        
src           └─┘     └─────┘     └─────┘          
typ           └─┘    └─────┘    └─────┘        
doc                   └─────┘     └─────┘
516    (∃ x, x ∈ s ∩ u) → (∃ x, x ∈ s ∩ v) → ∃ x, x ∈ s ∩ (u ∩ v)
id                                    
src                                              
typ                                   
517  
518  theorem is_connected_of_is_irreducible {s : set α} (H : is_irreducible s) : is_connected s :=
id                                               └─┘        └────────────┘     └──────────┘ 
src                                              └─┘         └────────────┘      └──────────┘
typ                                              └─┘        └────────────┘     └──────────┘ 
doc                                                          └────────────┘      └──────────┘
519  λ _ _ hu hv _, H _ _ hu hv
id       └┘ └┘        └┘ └┘
typ      └┘ └┘        └┘ └┘
520  
521  theorem is_connected_empty : is_connected (∅ : set α) :=
id                                └──────────┘     └─┘ 
src                               └──────────┘     └─┘
typ                               └──────────┘     └─┘ 
doc                               └──────────┘
522  is_connected_of_is_irreducible is_irreducible_empty
id   └────────────────────────────┘ └──────────────────┘
src  └────────────────────────────┘ └──────────────────┘
typ  └────────────────────────────┘ └──────────────────┘
523  
524  theorem is_connected_singleton {x} : is_connected ({x} : set α) :=
id                                        └──────────┘      └─┘ 
src                                       └──────────┘       └─┘
typ                                       └──────────┘      └─┘ 
doc                                       └──────────┘
525  is_connected_of_is_irreducible is_irreducible_singleton
id   └────────────────────────────┘ └──────────────────────┘
src  └────────────────────────────┘ └──────────────────────┘
typ  └────────────────────────────┘ └──────────────────────┘
526  
527  /-- If any point of a set is joined to a fixed point by a connected subset,
528  then the original set is connected as well. -/
529  theorem is_connected_of_forall {s : set α} (x : α)
id                                       └─┘        
src                                      └─┘
typ                                      └─┘        
530    (H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ is_connected t) :
id                              └──────────┘ 
src                                     └──────────┘
typ                             └──────────┘ 
doc                                           └──────────┘
531    is_connected s :=
id     └──────────┘ 
src    └──────────┘
typ    └──────────┘ 
doc    └──────────┘
532  begin
st   └─────
533    rintros u v hu hv hs ⟨z, zs, zu⟩ ⟨y, ys, yv⟩,
src    └──────────────────────────────────────────┘
typ    └──────────────────────────────────────────┘
doc    └──────────────────────────────────────────┘
txt    └──────────────────────────────────────────┘
par    └──────────────────────────────────────────┘
pid           └───────────────────────────────────┘
st   ─────────────────────────────────────────────┘└─
534    have xs : x ∈ s, by { rcases H y ys with ⟨t, ts, xt, yt, ht⟩, exact ts xt },
id                                 └┘                                 └┘ └┘
src    └────────┘         └─────┘    └───────────────────────┘  └────┘    
typ    └────────┘       └─────┘└┘└───────────────────────┘  └────┘└┘└┘
doc    └────────┘          └─────┘    └───────────────────────┘  └────┘    
txt    └────────┘          └─────┘    └───────────────────────┘  └────┘    
par    └────────┘          └─────┘    └───────────────────────┘  └────┘    
pid    └─────┘└─┘                    └───────────────────────┘           
st   ────────────────┘     └─────────────────────────────────────┘└────────────┘└┘
535    wlog xu : x ∈ u := hs xs using [u v y z, v u z y],
id                      └┘ └┘
src    └────────┘   └──┘    └───────────────────────┘
typ    └────────┘ └──┘└┘└┘└───────────────────────┘
doc    └────────┘   └──┘    └───────────────────────┘
txt    └────────┘   └──┘    └───────────────────────┘
par    └────────┘   └──┘    └───────────────────────┘
pid        └─┘└─┘   └──┘    └───────────────────────┘
st   ──────────────────────────────────────────────────┘└─
536    { rcases H y ys with ⟨t, ts, xt, yt, ht⟩,
id                └┘
src      └─────┘    └───────────────────────┘
typ      └─────┘└┘└───────────────────────┘
doc      └─────┘    └───────────────────────┘
txt      └─────┘    └───────────────────────┘
par      └─────┘    └───────────────────────┘
pid                └───────────────────────┘
st   ───┘└────────────────────────────────────┘└─
537      have := ht u v hu hv(subset.trans ts hs) ⟨x, xt, xu⟩ ⟨y, yt, yv⟩,
id               └┘   └┘ └┘ └──────────┘ └┘ └┘     └┘  └┘     └┘  └┘
src      └──────┘         └──────────┘    └┘  └┘  └┘  └┘  └┘  └┘  
typ      └──────┘└┘└┘└┘ └──────────┘└┘└┘└┘ └┘└┘└┘└┘└┘ └┘└┘└┘└┘
doc      └──────┘                         └┘  └┘  └┘  └┘  └┘  └┘  
txt      └──────┘                         └┘  └┘  └┘  └┘  └┘  └┘  
par      └──────┘                         └┘  └┘  └┘  └┘  └┘  └┘  
pid      └───┘└─┘                         └┘  └┘  └┘  └┘  └┘  └┘  
st   ───────────────────────────────────────────────────────────────────┘└─
538      exact this.imp (λ z hz, ⟨ts hz.1, hz.2⟩) },
id             └──────┘           └┘
src      └────┘└──────┘  └─────┘     └──┘  └───┘
typ      └────┘└──────┘  └─────┘ └┘  └──┘  └───┘
doc      └────┘          └─────┘     └──┘  └───┘
txt      └────┘          └─────┘     └──┘  └───┘
par      └────┘          └─────┘     └──┘  └───┘
pid                     └─────┘     └──┘  └──┘
st   ────────────────────────────────────────────┘└┘
539    { rw [union_comm v, inter_comm v] at this,
id           └────────┘   └────────┘ 
src      └──┘└────────┘ └┘└────────┘ └───────┘
typ      └──┘└────────┘└┘└────────┘└───────┘
doc      └──┘           └┘           └───────┘
txt      └──┘           └┘           └───────┘
par      └──┘           └┘           └───────┘
pid        └┘           └┘           └──────┘
st   ───────────────────┘└────────────┘└──────┘└─
540      apply this; assumption }
src      └────┘      └─────────┘
typ      └────┘      └─────────┘
doc      └────┘      └─────────┘
txt      └────┘      └─────────┘
par      └────┘      └─────────┘
pid                           
st   ──────────────────────────┘└─
541  end
st   ──┘
542  
543  /-- If any two points of a set are contained in a connected subset,
544  then the original set is connected as well. -/
545  theorem is_connected_of_forall_pair {s : set α}
id                                            └─┘ 
src                                           └─┘
typ                                           └─┘ 
546    (H : ∀ x y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ is_connected t) :
id                               └──────────┘ 
src                                       └──────────┘
typ                              └──────────┘ 
doc                                             └──────────┘
547    is_connected s :=
id     └──────────┘ 
src    └──────────┘
typ    └──────────┘ 
doc    └──────────┘
548  begin
st   └─────
549    rintros u v hu hv hs ⟨x, xs, xu⟩ ⟨y, ys, yv⟩,
src    └──────────────────────────────────────────┘
typ    └──────────────────────────────────────────┘
doc    └──────────────────────────────────────────┘
txt    └──────────────────────────────────────────┘
par    └──────────────────────────────────────────┘
pid           └───────────────────────────────────┘
st   ─────────────────────────────────────────────┘└─
550    rcases H x y xs ys with ⟨t, ts, xt, yt, ht⟩,
id               └┘ └┘
src    └─────┘       └───────────────────────┘
typ    └─────┘└┘└┘└───────────────────────┘
doc    └─────┘       └───────────────────────┘
txt    └─────┘       └───────────────────────┘
par    └─────┘       └───────────────────────┘
pid                 └───────────────────────┘
st   ────────────────────────────────────────────┘└─
551    have := ht u v hu hv(subset.trans ts hs) ⟨x, xt, xu⟩ ⟨y, yt, yv⟩,
id             └┘   └┘ └┘ └──────────┘ └┘ └┘     └┘  └┘     └┘  └┘
src    └──────┘         └──────────┘    └┘  └┘  └┘  └┘  └┘  └┘  
typ    └──────┘└┘└┘└┘ └──────────┘└┘└┘└┘ └┘└┘└┘└┘└┘ └┘└┘└┘└┘
doc    └──────┘                         └┘  └┘  └┘  └┘  └┘  └┘  
txt    └──────┘                         └┘  └┘  └┘  └┘  └┘  └┘  
par    └──────┘                         └┘  └┘  └┘  └┘  └┘  └┘  
pid    └───┘└─┘                         └┘  └┘  └┘  └┘  └┘  └┘  
st   ─────────────────────────────────────────────────────────────────┘└─
552    exact this.imp (λ z hz, ⟨ts hz.1, hz.2⟩)
id           └──────┘           └┘
src    └────┘└──────┘  └─────┘     └──┘  └───┘
typ    └────┘└──────┘  └─────┘ └┘  └──┘  └───┘
doc    └────┘          └─────┘     └──┘  └───┘
txt    └────┘          └─────┘     └──┘  └───┘
par    └────┘          └─────┘     └──┘  └───┘
pid                   └─────┘     └──┘  └──┘
st   ──────────────────────────────────────────┘
553  end
st   └─┘
554  
555  /-- A union of a family of connected sets with a common point is connected as well. -/
556  theorem is_connected_sUnion (x : α) (c : set (set α)) (H1 : ∀ s ∈ c, x ∈ s)
id                                           └─┘  └─┘                   
src                                           └─┘  └─┘                      
typ                                          └─┘  └─┘                   
557    (H2 : ∀ s ∈ c, is_connected s) : is_connected (⋃₀ c) :=
id                  └──────────┘     └──────────┘  └┘ 
src                   └──────────┘      └──────────┘  └┘
typ                 └──────────┘     └──────────┘  └┘ 
doc                   └──────────┘      └──────────┘
558  begin
st   └─────
559    apply is_connected_of_forall x,
id           └────────────────────┘ 
src    └────┘└────────────────────┘
typ    └────┘└────────────────────┘
doc    └────┘└────────────────────┘
txt    └────┘                      
par    └────┘                      
pid                               
st   ───────────────────────────────┘└─
560    rintros y ⟨s, sc, ys⟩,
src    └───────────────────┘
typ    └───────────────────┘
doc    └───────────────────┘
txt    └───────────────────┘
par    └───────────────────┘
pid           └────────────┘
st   ──────────────────────┘└─
561    exact ⟨s, subset_sUnion_of_mem sc, H1 s sc, ys, H2 s sc⟩
id               └──────────────────┘     └┘       └┘  └┘  └┘
src    └────┘  └┘└──────────────────┘  └┘     └┘  └┘     └┘
typ    └────┘  └┘└──────────────────┘  └┘└┘   └┘└┘└┘└┘└┘└┘
doc    └────┘  └┘                      └┘     └┘  └┘     └┘
txt    └────┘  └┘                      └┘     └┘  └┘     └┘
par    └────┘  └┘                      └┘     └┘  └┘     └┘
pid           └┘                      └┘     └┘  └┘     
st   ──────────────────────────────────────────────────────────┘
562  end
st   └─┘
563  
564  theorem is_connected.union (x : α) {s t : set α} (H1 : x ∈ s) (H2 : x ∈ t)
id                                            └─┘                     
src                                            └─┘                        
typ                                           └─┘                     
565    (H3 : is_connected s) (H4 : is_connected t) : is_connected (s ∪ t) :=
id           └──────────┘         └──────────┘     └──────────┘    
src          └──────────┘          └──────────┘      └──────────┘    
typ          └──────────┘         └──────────┘     └──────────┘    
doc          └──────────┘          └──────────┘      └──────────┘
566  sUnion_pair s t ▸ is_connected_sUnion x {s, t}
id   └─────────┘    └─────────────────┘   
src  └─────────┘      └─────────────────┘    
typ  └─────────┘    └─────────────────┘   
doc                    └─────────────────┘
567    (by rintro r (rfl | rfl | h); [exact H2, exact H1, exact h.elim])
id                                         └┘        └┘        └────┘
src        └──────────────────────┘  └────┘    └────┘    └────┘└────┘
typ        └──────────────────────┘  └────┘└┘  └────┘└┘  └────┘└────┘
doc        └──────────────────────┘   └────┘    └────┘    └────┘
txt        └──────────────────────┘   └────┘    └────┘    └────┘
par        └──────────────────────┘   └────┘    └────┘    └────┘
pid              └────────────────┘                          
st        └───────────────────────────────────────────────────────────┘
568    (by rintro r (rfl | rfl | h); [exact H4, exact H3, exact h.elim])
id                                         └┘        └┘        └────┘
src        └──────────────────────┘  └────┘    └────┘    └────┘└────┘
typ        └──────────────────────┘  └────┘└┘  └────┘└┘  └────┘└────┘
doc        └──────────────────────┘   └────┘    └────┘    └────┘
txt        └──────────────────────┘   └────┘    └────┘    └────┘
par        └──────────────────────┘   └────┘    └────┘    └────┘
pid              └────────────────┘                          
st        └───────────────────────────────────────────────────────────┘
569  
570  theorem is_connected.closure {s : set α} (H : is_connected s) :
id                                     └─┘        └──────────┘ 
src                                    └─┘         └──────────┘
typ                                    └─┘        └──────────┘ 
doc                                                └──────────┘
571    is_connected (closure s) :=
id     └──────────┘  └─────┘ 
src    └──────────┘  └─────┘
typ    └──────────┘  └─────┘ 
doc    └──────────┘  └─────┘
572  λ u v hu hv hcsuv ⟨y, hycs, hyu⟩ ⟨z, hzcs, hzv⟩,
id       └┘ └┘ └───┘    └──┘  └─┘     └──┘  └─┘
typ      └┘ └┘ └───┘    └──┘  └─┘     └──┘  └─┘
573  let ⟨p, hpu, hps⟩ := mem_closure_iff.1 hycs u hu hyu in
id   └─┘    └─┘  └─┘     └─────────────┘        └┘
src                       └─────────────┘
typ  └─┘    └─┘  └─┘     └─────────────┘        └┘
574  let ⟨q, hqv, hqs⟩ := mem_closure_iff.1 hzcs v hv hzv in
id   └─┘    └─┘  └─┘     └─────────────┘        └┘
src                       └─────────────┘
typ  └─┘    └─┘  └─┘     └─────────────┘        └┘
575  let ⟨r, hrs, hruv⟩ := H u v hu hv (subset.trans subset_closure hcsuv) ⟨p, hps, hpu⟩ ⟨q, hqs, hqv⟩ in
id   └─┘    └─┘  └──┘        └┘ └┘  └──────────┘ └────────────┘ └───┘
src                                     └──────────┘ └────────────┘
typ  └─┘    └─┘  └──┘        └┘ └┘  └──────────┘ └────────────┘ └───┘
576  ⟨r, subset_closure hrs, hruv⟩
id       └────────────┘
src      └────────────┘
typ      └────────────┘
577  
578  theorem is_connected.image [topological_space β] {s : set α} (H : is_connected s)
id                               └───────────────┘        └─┘        └──────────┘ 
src                              └───────────────┘         └─┘         └──────────┘
typ                              └───────────────┘        └─┘        └──────────┘ 
doc                              └───────────────┘                     └──────────┘
579    (f : α → β) (hf : continuous_on f s) : is_connected (f '' s) :=
id                     └───────────┘      └──────────┘   └┘ 
src                      └───────────┘        └──────────┘    └┘
typ                    └───────────┘      └──────────┘   └┘ 
doc                      └───────────┘        └──────────┘
580  begin
st   └─────
581    -- Unfold/destruct definitions in hypotheses
st   ───────────────────────────────────────────────
582    rintros u v hu hv huv ⟨_, ⟨x, xs, rfl⟩, xu⟩ ⟨_, ⟨y, ys, rfl⟩, yv⟩,
src    └───────────────────────────────────────────────────────────────┘
typ    └───────────────────────────────────────────────────────────────┘
doc    └───────────────────────────────────────────────────────────────┘
txt    └───────────────────────────────────────────────────────────────┘
par    └───────────────────────────────────────────────────────────────┘
pid           └────────────────────────────────────────────────────────┘
st   ──────────────────────────────────────────────────────────────────┘└─
583    rcases continuous_on_iff'.1 hf u hu with ⟨u', hu', u'_eq⟩,
id            └────────────────┘   └┘  └┘
src    └─────┘└────────────────┘└─┘     └────────────────────┘
typ    └─────┘└────────────────┘└─┘└┘└┘└────────────────────┘
doc    └─────┘                  └─┘     └────────────────────┘
txt    └─────┘                  └─┘     └────────────────────┘
par    └─────┘                  └─┘     └────────────────────┘
pid                            └─┘     └────────────────────┘
st   ──────────────────────────────────────────────────────────┘└─
584    rcases continuous_on_iff'.1 hf v hv with ⟨v', hv', v'_eq⟩,
id            └────────────────┘   └┘  └┘
src    └─────┘└────────────────┘└─┘     └────────────────────┘
typ    └─────┘└────────────────┘└─┘└┘└┘└────────────────────┘
doc    └─────┘                  └─┘     └────────────────────┘
txt    └─────┘                  └─┘     └────────────────────┘
par    └─────┘                  └─┘     └────────────────────┘
pid                            └─┘     └────────────────────┘
st   ──────────────────────────────────────────────────────────┘└─
585    -- Reformulate `huv : f '' s ⊆ u ∪ v` in terms of `u'` and `v'`
st   ──────────────────────────────────────────────────────────────────
586    replace huv : s ⊆ u' ∪ v',
id                     └┘  └┘
src    └────────────┘   
typ    └────────────┘└┘└┘
doc    └────────────┘     
txt    └────────────┘     
par    └────────────┘     
pid           └──┘└─┘     
st   ──────────────────────────┘└─
587    { rw [image_subset_iff, preimage_union] at huv,
id           └──────────────┘  └────────────┘
src      └──┘└──────────────┘└┘└────────────┘└──────┘
typ      └──┘└──────────────┘└┘└────────────┘└──────┘
doc      └──┘└──────────────┘└┘              └──────┘
txt      └──┘                └┘              └──────┘
par      └──┘                └┘              └──────┘
pid        └┘                └┘              └─────┘
st   ───┘└──────────────────┘└──────────────┘└─────┘└─
588      replace huv := subset_inter huv (subset.refl _),
id                      └──────────┘ └─┘  └─────────┘
src      └─────────────┘└──────────┘    └─────────┘└─┘
typ      └─────────────┘└──────────┘└─┘ └─────────┘└─┘
doc      └─────────────┘                           └─┘
txt      └─────────────┘                           └─┘
par      └─────────────┘                           └─┘
pid             └──┘└─┘                           └─┘
st   ──────────────────────────────────────────────────┘└─
589      rw [inter_distrib_right, u'_eq, v'_eq, ← inter_distrib_right] at huv,
id           └─────────────────┘  └───┘  └───┘    └─────────────────┘
src      └──┘└─────────────────┘└┘     └┘     └──┘└─────────────────┘└──────┘
typ      └──┘└─────────────────┘└┘└───┘└┘└───┘└──┘└─────────────────┘└──────┘
doc      └──┘                   └┘     └┘     └──┘                   └──────┘
txt      └──┘                   └┘     └┘     └──┘                   └──────┘
par      └──┘                   └┘     └┘     └──┘                   └──────┘
pid        └┘                   └┘     └┘     └──┘                   └─────┘
st   ──────────────────────────┘└─────┘└─────┘└─────────────────────┘└─────┘└─
590      exact (subset_inter_iff.1 huv).1 },
id              └──────────────┘   └─┘
src      └────┘ └──────────────┘└─┘   └──┘
typ      └────┘ └──────────────┘└─┘└─┘└──┘
doc      └────┘                 └─┘   └──┘
txt      └────┘                 └─┘   └──┘
par      └────┘                 └─┘   └──┘
pid                            └─┘   └─┘
st   ────────────────────────────────────┘└┘
591    -- Now `s ⊆ u' ∪ v'`, so we can apply `‹is_connected s›`
st   ───────────────────────────────────────────────────────────
592    obtain ⟨z, hz⟩ : (s ∩ (u' ∩ v')).nonempty,
id                          └┘   └┘
src    └───────────────┘        └─────────┘
typ    └───────────────┘  └┘ └┘└─────────┘
doc    └───────────────┘         └─────────┘
txt    └───────────────┘         └─────────┘
par    └───────────────┘         └─────────┘
pid          └─────────┘         └────────┘
st   ──────────────────────────────────────────┘└─
593    { refine H u' v' hu' hv' huv ⟨x, _⟩ ⟨y, _⟩; rw inter_comm,
id               └┘ └┘ └─┘ └─┘ └─┘                 └────────┘
src      └─────┘                └───┘  └──┘  └─┘└────────┘
typ      └─────┘└┘└┘└─┘└─┘└─┘ └───┘ └──┘  └─┘└────────┘
doc      └─────┘                └───┘  └──┘  └─┘
txt      └─────┘                └───┘  └──┘  └─┘
par      └─────┘                └───┘  └──┘  └─┘
pid                            └───┘  └──┘    
st   ───┘└───────────────────────────────────────────┘└────────┘└─
594      exacts [u'_eq ▸ ⟨xu, xs⟩, v'_eq ▸ ⟨yv, ys⟩] },
id               └───┘   └┘  └┘   └───┘    └┘  └┘
src      └──────┘        └┘  └─┘         └┘  └─┘
typ      └──────┘└───┘ └┘└┘└┘└─┘└───┘  └┘└┘└┘└─┘
doc      └──────┘         └┘  └─┘         └┘  └─┘
txt      └──────┘         └┘  └─┘         └┘  └─┘
par      └──────┘         └┘  └─┘         └┘  └─┘
pid            └┘         └┘  └─┘         └┘  └┘
st   ───────────────────────────────────────────────┘└┘
595    rw [← inter_self s, inter_assoc, inter_left_comm s u', ← inter_assoc,
id           └────────┘   └─────────┘  └─────────────┘  └┘    └─────────┘
src    └────┘└────────┘ └┘└─────────┘└┘└─────────────┘   └──┘└─────────┘└─
typ    └────┘└────────┘└┘└─────────┘└┘└─────────────┘└┘└──┘└─────────┘└─
doc    └────┘           └┘           └┘                  └──┘           └─
txt    └────┘           └┘           └┘                  └──┘           └─
par    └────┘           └┘           └┘                  └──┘           └─
pid      └──┘           └┘           └┘                  └──┘           └─
st   ───────────────────┘└───────────┘└────────────────────┘└─────────────┘└─
596      inter_comm s, inter_comm s, ← u'_eq, ← v'_eq] at hz,
id       └────────┘   └────────┘     └───┘    └───┘
src  ───┘└────────┘ └┘└────────┘ └──┘     └──┘     └─────┘
typ  ───┘└────────┘└┘└────────┘└──┘└───┘└──┘└───┘└─────┘
doc  ───┘           └┘           └──┘     └──┘     └─────┘
txt  ───┘           └┘           └──┘     └──┘     └─────┘
par  ───┘           └┘           └──┘     └──┘     └─────┘
pid  ───┘           └┘           └──┘     └──┘     └────┘
st   ───────────────┘└────────────┘└───────┘└───────┘└────┘└─
597    exact ⟨f z, ⟨z, hz.1.2, rfl⟩, hz.1.1, hz.2.1⟩
id                           └─┘           └┘
src    └────┘   └┘  └┘  └────┘└─┘└─┘  └────┘  └────┘
typ    └────┘  └┘ └┘  └────┘└─┘└─┘  └────┘└┘└────┘
doc    └────┘   └┘  └┘  └────┘   └─┘  └────┘  └────┘
txt    └────┘   └┘  └┘  └────┘   └─┘  └────┘  └────┘
par    └────┘   └┘  └┘  └────┘   └─┘  └────┘  └────┘
pid            └┘  └┘  └────┘   └─┘  └────┘  └───┘
st   ───────────────────────────────────────────────┘
598  end
st   └─┘
599  
600  theorem is_connected_closed_iff {s : set α} :
id                                        └─┘ 
src                                       └─┘
typ                                       └─┘ 
601    is_connected s ↔ ∀ t t', is_closed t → is_closed t' → s ⊆ t ∪ t' →
id     └──────────┘      └┘  └───────┘    └───────┘ └┘       └┘
src    └──────────┘            └───────┘     └───────┘           
typ    └──────────┘      └┘  └───────┘    └───────┘ └┘       └┘
doc    └──────────┘             └───────┘     └───────┘
602      (s ∩ t).nonempty → (s ∩ t').nonempty → (s ∩ (t ∩ t')).nonempty :=
id           └──────┘       └┘ └──────┘          └┘  └──────┘
src            └──────┘           └──────┘                └──────┘
typ          └──────┘       └┘ └──────┘          └┘  └──────┘
doc             └──────┘            └──────┘                  └──────┘
603  ⟨begin
st    └─────
604    rintros h t t' ht ht' htt' ⟨x, xs, xt⟩ ⟨y, ys, yt'⟩,
src    └─────────────────────────────────────────────────┘
typ    └─────────────────────────────────────────────────┘
doc    └─────────────────────────────────────────────────┘
txt    └─────────────────────────────────────────────────┘
par    └─────────────────────────────────────────────────┘
pid           └──────────────────────────────────────────┘
st   ────────────────────────────────────────────────────┘└─
605    by_contradiction h',
src    └─────────────────┘
typ    └─────────────────┘
doc    └─────────────────┘
txt    └─────────────────┘
par    └─────────────────┘
pid                    └─┘
st   ────────────────────┘└─
606    rw [← ne_empty_iff_nonempty, ne.def, not_not, ← subset_compl_iff_disjoint, compl_inter] at h',
id           └───────────────────┘  └────┘  └─────┘    └───────────────────────┘  └─────────┘
src    └────┘└───────────────────┘└┘└────┘└┘└─────┘└──┘└───────────────────────┘└┘└─────────┘└─────┘
typ    └────┘└───────────────────┘└┘└────┘└┘└─────┘└──┘└───────────────────────┘└┘└─────────┘└─────┘
doc    └────┘                     └┘      └┘       └──┘                         └┘           └─────┘
txt    └────┘                     └┘      └┘       └──┘                         └┘           └─────┘
par    └────┘                     └┘      └┘       └──┘                         └┘           └─────┘
pid      └──┘                     └┘      └┘       └──┘                         └┘           └────┘
st   ────────────────────────────┘└──────┘└───────┘└───────────────────────────┘└───────────┘└────┘└─
607    have xt' : x ∉ t', from (h' xs).elim (absurd xt) id,
id                  └┘        └┘ └┘        └────┘ └┘  └┘
src    └─────────┘     └───┘     └─────┘ └────┘  └┘└┘
typ    └─────────┘└┘  └───┘ └┘└┘└─────┘ └────┘└┘└┘└┘
doc    └─────────┘      └───┘     └─────┘         └┘
txt    └─────────┘      └───┘     └─────┘         └┘
par    └─────────┘      └───┘     └─────┘         └┘
pid    └──────┘└─┘      └───┘     └─────┘         └┘
st   ──────────────────┘└────────────────────────────────┘└─
608    have yt : y ∉ t, from (h' ys).elim id (absurd yt'),
id                          └┘ └┘       └┘  └────┘ └─┘
src    └────────┘     └───┘     └─────┘└┘ └────┘   
typ    └────────┘   └───┘ └┘└┘└─────┘└┘ └────┘└─┘
doc    └────────┘     └───┘     └─────┘            
txt    └────────┘     └───┘     └─────┘            
par    └────────┘     └───┘     └─────┘            
pid    └─────┘└─┘     └───┘     └─────┘            
st   ────────────────┘└─────────────────────────────────┘└─
609    have := ne_empty_iff_nonempty.2 (h (-t) (-t') (is_open_compl_iff.2 ht)
id             └───────────────────┘          └┘                       └┘
src    └──────┘└───────────────────┘└─┘    └┘    └┘                  └─┘  └─
typ    └──────┘└───────────────────┘└─┘  └┘  └┘└┘                  └─┘└┘└─
doc    └──────┘                     └─┘     └┘    └┘                  └─┘  └─
txt    └──────┘                     └─┘     └┘    └┘                  └─┘  └─
par    └──────┘                     └─┘     └┘    └┘                  └─┘  └─
pid    └───┘└─┘                     └─┘     └┘    └┘                  └─┘  └─
st   ─────────────────────────────────────────────────────────────────────────
610      (is_open_compl_iff.2 ht') h' ⟨y, ys, yt⟩ ⟨x, xs, xt'⟩),
id        └───────────────┘   └─┘  └┘    └┘  └┘     └┘  └─┘
src  ───┘ └───────────────┘└─┘   └┘    └┘  └┘  └┘  └┘  └┘   └┘
typ  ───┘ └───────────────┘└─┘└─┘└┘└┘ └┘└┘└┘└┘└┘ └┘└┘└┘└─┘└┘
doc  ───┘                  └─┘   └┘    └┘  └┘  └┘  └┘  └┘   └┘
txt  ───┘                  └─┘   └┘    └┘  └┘  └┘  └┘  └┘   └┘
par  ───┘                  └─┘   └┘    └┘  └┘  └┘  └┘  └┘   └┘
pid  ───┘                  └─┘   └┘    └┘  └┘  └┘  └┘  └┘   └┘
st   ─────────────────────────────────────────────────────────┘└─
611    rw [ne.def, ← compl_union, ← subset_compl_iff_disjoint, compl_compl] at this,
id         └────┘    └─────────┘    └───────────────────────┘  └─────────┘
src    └──┘└────┘└──┘└─────────┘└──┘└───────────────────────┘└┘└─────────┘└───────┘
typ    └──┘└────┘└──┘└─────────┘└──┘└───────────────────────┘└┘└─────────┘└───────┘
doc    └──┘      └──┘           └──┘                         └┘           └───────┘
txt    └──┘      └──┘           └──┘                         └┘           └───────┘
par    └──┘      └──┘           └──┘                         └┘           └───────┘
pid      └┘      └──┘           └──┘                         └┘           └──────┘
st   ───────────┘└─────────────┘└───────────────────────────┘└───────────┘└──────┘└─
612    contradiction
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid                 
st   ───────────────┘
613  end,
st   └─┘
614  begin
st   └─────
615    rintros h u v hu hv huv ⟨x, xs, xu⟩ ⟨y, ys, yv⟩,
src    └─────────────────────────────────────────────┘
typ    └─────────────────────────────────────────────┘
doc    └─────────────────────────────────────────────┘
txt    └─────────────────────────────────────────────┘
par    └─────────────────────────────────────────────┘
pid           └──────────────────────────────────────┘
st   ────────────────────────────────────────────────┘└─
616    by_contradiction h',
src    └─────────────────┘
typ    └─────────────────┘
doc    └─────────────────┘
txt    └─────────────────┘
par    └─────────────────┘
pid                    └─┘
st   ────────────────────┘└─
617    rw [← set.nonempty, ← ne_empty_iff_nonempty, ne.def, not_not,
id           └──────────┘    └───────────────────┘  └────┘  └─────┘
src    └────┘└──────────┘└──┘└───────────────────┘└┘└────┘└┘└─────┘└─
typ    └────┘└──────────┘└──┘└───────────────────┘└┘└────┘└┘└─────┘└─
doc    └────┘└──────────┘└──┘                     └┘      └┘       └─
txt    └────┘            └──┘                     └┘      └┘       └─
par    └────┘            └──┘                     └┘      └┘       └─
pid      └──┘            └──┘                     └┘      └┘       └─
st   ───────────────────┘└───────────────────────┘└──────┘└───────┘└─
618      ← subset_compl_iff_disjoint, compl_inter] at h',
id         └───────────────────────┘  └─────────┘
src  ─────┘└───────────────────────┘└┘└─────────┘└─────┘
typ  ─────┘└───────────────────────┘└┘└─────────┘└─────┘
doc  ─────┘                         └┘           └─────┘
txt  ─────┘                         └┘           └─────┘
par  ─────┘                         └┘           └─────┘
pid  ─────┘                         └┘           └────┘
st   ──────────────────────────────┘└───────────┘└────┘└─
619    have xv : x ∉ v, from (h' xs).elim (absurd xu) id,
id                          └┘ └┘        └────┘ └┘  └┘
src    └────────┘     └───┘     └─────┘ └────┘  └┘└┘
typ    └────────┘   └───┘ └┘└┘└─────┘ └────┘└┘└┘└┘
doc    └────────┘     └───┘     └─────┘         └┘
txt    └────────┘     └───┘     └─────┘         └┘
par    └────────┘     └───┘     └─────┘         └┘
pid    └─────┘└─┘     └───┘     └─────┘         └┘
st   ────────────────┘└────────────────────────────────┘└─
620    have yu : y ∉ u, from (h' ys).elim id (absurd yv),
id                          └┘ └┘       └┘  └────┘ └┘
src    └────────┘     └───┘     └─────┘└┘ └────┘  
typ    └────────┘   └───┘ └┘└┘└─────┘└┘ └────┘└┘
doc    └────────┘     └───┘     └─────┘           
txt    └────────┘     └───┘     └─────┘           
par    └────────┘     └───┘     └─────┘           
pid    └─────┘└─┘     └───┘     └─────┘           
st   ────────────────┘└────────────────────────────────┘└─
621    have := ne_empty_iff_nonempty.2 (h (-u) (-v) (is_closed_compl_iff.2 hu)
id             └───────────────────┘                                    └┘
src    └──────┘└───────────────────┘└─┘     └┘   └┘                    └─┘  └─
typ    └──────┘└───────────────────┘└─┘   └┘  └┘                    └─┘└┘└─
doc    └──────┘                     └─┘     └┘   └┘                    └─┘  └─
txt    └──────┘                     └─┘     └┘   └┘                    └─┘  └─
par    └──────┘                     └─┘     └┘   └┘                    └─┘  └─
pid    └───┘└─┘                     └─┘     └┘   └┘                    └─┘  └─
st   ──────────────────────────────────────────────────────────────────────────
622      (is_closed_compl_iff.2 hv) h' ⟨y, ys, yu⟩ ⟨x, xs, xv⟩),
id        └─────────────────┘   └┘  └┘    └┘  └┘     └┘  └┘
src  ───┘ └─────────────────┘└─┘  └┘    └┘  └┘  └┘  └┘  └┘  └┘
typ  ───┘ └─────────────────┘└─┘└┘└┘└┘ └┘└┘└┘└┘└┘ └┘└┘└┘└┘└┘
doc  ───┘                    └─┘  └┘    └┘  └┘  └┘  └┘  └┘  └┘
txt  ───┘                    └─┘  └┘    └┘  └┘  └┘  └┘  └┘  └┘
par  ───┘                    └─┘  └┘    └┘  └┘  └┘  └┘  └┘  └┘
pid  ───┘                    └─┘  └┘    └┘  └┘  └┘  └┘  └┘  └┘
st   ─────────────────────────────────────────────────────────┘└─
623    rw [ne.def, ← compl_union, ← subset_compl_iff_disjoint, compl_compl] at this,
id         └────┘    └─────────┘    └───────────────────────┘  └─────────┘
src    └──┘└────┘└──┘└─────────┘└──┘└───────────────────────┘└┘└─────────┘└───────┘
typ    └──┘└────┘└──┘└─────────┘└──┘└───────────────────────┘└┘└─────────┘└───────┘
doc    └──┘      └──┘           └──┘                         └┘           └───────┘
txt    └──┘      └──┘           └──┘                         └┘           └───────┘
par    └──┘      └──┘           └──┘                         └┘           └───────┘
pid      └┘      └──┘           └──┘                         └┘           └──────┘
st   ───────────┘└─────────────┘└───────────────────────────┘└───────────┘└──────┘└─
624    contradiction
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid                 
st   ───────────────┘
625  end⟩
st   └─┘
626  
627  /-- The connected component of a point is the maximal connected set
628  that contains this point. -/
629  def connected_component (x : α) : set α :=
id                                    └─┘ 
src                                    └─┘
typ                                   └─┘ 
630  ⋃₀ { s : set α | is_connected s ∧ x ∈ s }
id   └┘      └─┘    └──────────┘     
src  └┘      └─┘     └──────────┘      
typ  └┘      └─┘    └──────────┘     
doc                   └──────────┘
631  
632  theorem is_connected_connected_component {x : α} : is_connected (connected_component x) :=
id                                                     └──────────┘  └─────────────────┘ 
src                                                     └──────────┘  └─────────────────┘
typ                                                    └──────────┘  └─────────────────┘ 
doc                                                     └──────────┘  └─────────────────┘
633  is_connected_sUnion x _ (λ _, and.right) (λ _, and.left)
id   └─────────────────┘         └───────┘       └──────┘
src  └─────────────────┘           └───────┘        └──────┘
typ  └─────────────────┘         └───────┘       └──────┘
doc  └─────────────────┘
634  
635  theorem mem_connected_component {x : α} : x ∈ connected_component x :=
id                                              └─────────────────┘ 
src                                               └─────────────────┘
typ                                             └─────────────────┘ 
doc                                                └─────────────────┘
636  mem_sUnion_of_mem (mem_singleton x) ⟨is_connected_singleton, mem_singleton x⟩
id   └───────────────┘  └───────────┘    └────────────────────┘  └───────────┘ 
src  └───────────────┘  └───────────┘     └────────────────────┘  └───────────┘
typ  └───────────────┘  └───────────┘    └────────────────────┘  └───────────┘ 
637  
638  theorem subset_connected_component {x : α} {s : set α} (H1 : is_connected s) (H2 : x ∈ s) :
id                                                  └─┘         └──────────┘           
src                                                  └─┘          └──────────┘            
typ                                                 └─┘         └──────────┘           
doc                                                               └──────────┘
639    s ⊆ connected_component x :=
id       └─────────────────┘ 
src       └─────────────────┘
typ      └─────────────────┘ 
doc        └─────────────────┘
640  λ z hz, mem_sUnion_of_mem hz ⟨H1, H2⟩
id      └┘  └───────────────┘ └┘  └┘  └┘
src          └───────────────┘
typ     └┘  └───────────────┘ └┘  └┘  └┘
641  
642  theorem is_closed_connected_component {x : α} :
id                                              
typ                                             
643    is_closed (connected_component x) :=
id     └───────┘  └─────────────────┘ 
src    └───────┘  └─────────────────┘
typ    └───────┘  └─────────────────┘ 
doc    └───────┘  └─────────────────┘
644  closure_eq_iff_is_closed.1 $ subset.antisymm
id   └──────────────────────┘    └─────────────┘
src  └──────────────────────┘    └─────────────┘
typ  └──────────────────────┘    └─────────────┘
645    (subset_connected_component
id      └────────────────────────┘
src     └────────────────────────┘
typ     └────────────────────────┘
646      is_connected_connected_component.closure
id       └──────────────────────────────┘└──────┘
src      └──────────────────────────────┘└──────┘
typ      └──────────────────────────────┘└──────┘
647      (subset_closure mem_connected_component))
id        └────────────┘ └─────────────────────┘
src       └────────────┘ └─────────────────────┘
typ       └────────────┘ └─────────────────────┘
648    subset_closure
id     └────────────┘
src    └────────────┘
typ    └────────────┘
649  
650  theorem irreducible_component_subset_connected_component {x : α} :
id                                                                 
typ                                                                
651    irreducible_component x ⊆ connected_component x :=
id     └───────────────────┘   └─────────────────┘ 
src    └───────────────────┘    └─────────────────┘
typ    └───────────────────┘   └─────────────────┘ 
doc    └───────────────────┘     └─────────────────┘
652  subset_connected_component
id   └────────────────────────┘
src  └────────────────────────┘
typ  └────────────────────────┘
653    (is_connected_of_is_irreducible is_irreducible_irreducible_component)
id      └────────────────────────────┘ └──────────────────────────────────┘
src     └────────────────────────────┘ └──────────────────────────────────┘
typ     └────────────────────────────┘ └──────────────────────────────────┘
654    mem_irreducible_component
id     └───────────────────────┘
src    └───────────────────────┘
typ    └───────────────────────┘
655  
656  /-- A connected space is one where there is no non-trivial open partition. -/
657  class connected_space (α : Type u) [topological_space α] : Prop :=
id                              └──┘     └───────────────┘ 
src                                      └───────────────┘
typ                             └──┘     └───────────────┘ 
doc                                      └───────────────┘
658  (is_connected_univ : is_connected (univ : set α))
id                        └──────────┘  └──┘   └─┘ 
src                       └──────────┘  └──┘   └─┘
typ                       └──────────┘  └──┘   └─┘ 
doc                       └──────────┘
659  
660  @[priority 100] -- see Note [lower instance priority]
661  instance irreducible_space.connected_space (α : Type u) [topological_space α]
id                                                            └───────────────┘ 
src                                                           └───────────────┘
typ                                                           └───────────────┘ 
doc                                                           └───────────────┘
662    [irreducible_space α] : connected_space α :=
id      └───────────────┘     └─────────────┘ 
src     └───────────────┘      └─────────────┘
typ     └───────────────┘     └─────────────┘ 
doc     └───────────────┘      └─────────────┘
663  ⟨is_connected_of_is_irreducible $ irreducible_space.is_irreducible_univ α⟩
id    └────────────────────────────┘   └───────────────────────────────────┘ 
src   └────────────────────────────┘   └───────────────────────────────────┘
typ   └────────────────────────────┘   └───────────────────────────────────┘ 
664  
665  theorem exists_mem_inter [connected_space α] {s t : set α} :
id                             └─────────────┘          └─┘ 
src                            └─────────────┘           └─┘
typ                            └─────────────┘          └─┘ 
doc                            └─────────────┘
666    is_open s → is_open t → s ∪ t = univ →
id     └─────┘    └─────┘        └──┘
src    └─────┘     └─────┘           └──┘
typ    └─────┘    └─────┘        └──┘
doc    └─────┘     └─────┘
667      (∃ x, x ∈ s) → (∃ x, x ∈ t) → ∃ x, x ∈ s ∩ t :=
id                               
src                                      
typ                              
668  by simpa only [univ_inter, univ_subset_iff] using
id                  └────────┘  └─────────────┘
src     └──────────┘└────────┘└┘└─────────────┘└───────
typ     └──────────┘└────────┘└┘└─────────────┘└───────
doc     └──────────┘          └┘               └───────
txt     └──────────┘          └┘               └───────
par     └──────────┘          └┘               └───────
pid          └──┘└┘          └┘               └─────
st     └───────────────────────────────────────────────
669    @connected_space.is_connected_univ α _ _ s t
id      └───────────────────────────────┘       
src  ─┘ └───────────────────────────────┘ └───┘  
typ  ─┘ └───────────────────────────────┘└───┘
doc  ─┘                                   └───┘  
txt  ─┘                                   └───┘  
par  ─┘                                   └───┘  
pid  ─┘                                   └───┘  
st   ───────────────────────────────────────────────
670  
src  
typ  
doc  
txt  
par  
pid  
st   
671  theorem is_clopen_iff [connected_space α] {s : set α} : is_clopen s ↔ s = ∅ ∨ s = univ :=
id                          └─────────────┘        └─┘     └───────┘         └──┘
src                         └─────────────┘         └─┘      └───────┘            └──┘
typ                         └─────────────┘        └─┘     └───────┘         └──┘
doc                         └─────────────┘                  └───────┘
672  ⟨λ hs, classical.by_contradiction $ λ h,
id      └┘  └────────────────────────┘     
src         └────────────────────────┘
typ     └┘  └────────────────────────┘     
673    have h1 : s ≠ ∅ ∧ -s ≠ ∅, from ⟨mt or.inl h,
id                             └┘ └────┘ 
src                              └┘ └────┘
typ                            └┘ └────┘ 
674      mt (λ h2, or.inr $ (by rw [← compl_compl s, h2, compl_empty] : s = univ)) h⟩,
id       └┘    └┘  └────┘             └─────────┘   └┘  └─────────┘      └──┘   
src      └┘        └────┘       └────┘└─────────┘ └┘  └┘└─────────┘└┘     └──┘
typ      └┘    └┘  └────┘       └────┘└─────────┘└┘└┘└┘└─────────┘└┘    └──┘   
doc                             └────┘            └┘  └┘           └┘
txt                             └────┘            └┘  └┘           └┘
par                             └────┘            └┘  └┘           └┘
pid                               └──┘            └┘  └┘           
st                             └──────────────────┘└──┘└───────────┘
675    let ⟨_, h2, h3⟩ := exists_mem_inter hs.1 hs.2 (union_compl_self s)
id     └─┘     └┘  └┘     └──────────────┘ └┘  └┘   └──────────────┘ 
src                       └──────────────┘          └──────────────┘
typ    └─┘     └┘  └┘     └──────────────┘ └┘  └┘   └──────────────┘ 
676      (ne_empty_iff_nonempty.1 h1.1) (ne_empty_iff_nonempty.1 h1.2) in
id        └───────────────────┘  └┘    └───────────────────┘  └┘
src       └───────────────────┘        └───────────────────┘    
typ       └───────────────────┘  └┘    └───────────────────┘  └┘
677    h3 h2,
678  by rintro (rfl | rfl); [exact is_clopen_empty, exact is_clopen_univ]⟩
id                                └─────────────┘        └────────────┘
src     └────────────────┘  └────┘└─────────────┘  └────┘└────────────┘
typ     └────────────────┘  └────┘└─────────────┘  └────┘└────────────┘
doc     └────────────────┘   └────┘                 └────┘
txt     └────────────────┘   └────┘                 └────┘
par     └────────────────┘   └────┘                 └────┘
pid           └──────────┘                              
st     └────────────────────────────────────────────────────────────────┘
679  
680  end connected
681  
682  section totally_disconnected
683  
684  /-- A set is called totally disconnected if all of its connected components are singletons. -/
685  def is_totally_disconnected (s : set α) : Prop :=
id                                    └─┘ 
src                                   └─┘
typ                                   └─┘ 
686  ∀ t, t ⊆ s → is_connected t → subsingleton t
id            └──────────┘    └──────────┘ 
src              └──────────┘     └──────────┘
typ           └──────────┘    └──────────┘ 
doc               └──────────┘
687  
688  theorem is_totally_disconnected_empty : is_totally_disconnected (∅ : set α) :=
id                                           └─────────────────────┘     └─┘ 
src                                          └─────────────────────┘     └─┘
typ                                          └─────────────────────┘     └─┘ 
doc                                          └─────────────────────┘
689  λ t ht _, ⟨λ ⟨_, h⟩, (ht h).elim⟩
id      └┘             └┘   └──┘
src                             └──┘
typ     └┘             └┘   └──┘
690  
691  theorem is_totally_disconnected_singleton {x} : is_totally_disconnected ({x} : set α) :=
id                                                   └─────────────────────┘      └─┘ 
src                                                  └─────────────────────┘       └─┘
typ                                                  └─────────────────────┘      └─┘ 
doc                                                  └─────────────────────┘
692  λ t ht _, ⟨λ ⟨p, hp⟩ ⟨q, hq⟩, subtype.eq $ show p = q,
id      └┘        └┘    └┘   └────────┘          
src                                └────────┘          
typ     └┘        └┘    └┘   └────────┘          
693  from (eq_of_mem_singleton (ht hp)).symm ▸ (eq_of_mem_singleton (ht hq)).symm⟩
id         └─────────────────┘  └┘     └──┘    └─────────────────┘  └┘     └──┘
src        └─────────────────┘         └──┘    └─────────────────┘         └──┘
typ        └─────────────────┘  └┘     └──┘    └─────────────────┘  └┘     └──┘
694  
695  /-- A space is totally disconnected if all of its connected components are singletons. -/
696  class totally_disconnected_space (α : Type u) [topological_space α] : Prop :=
id                                         └──┘     └───────────────┘ 
src                                                 └───────────────┘
typ                                        └──┘     └───────────────┘ 
doc                                                 └───────────────┘
697  (is_totally_disconnected_univ : is_totally_disconnected (univ : set α))
id                                   └─────────────────────┘  └──┘   └─┘ 
src                                  └─────────────────────┘  └──┘   └─┘
typ                                  └─────────────────────┘  └──┘   └─┘ 
doc                                  └─────────────────────┘
698  
699  end totally_disconnected
700  
701  section totally_separated
702  
703  /-- A set `s` is called totally separated if any two points of this set can be separated
704  by two disjoint open sets covering `s`. -/
705  def is_totally_separated (s : set α) : Prop :=
id                                 └─┘ 
src                                └─┘
typ                                └─┘ 
706  ∀ x ∈ s, ∀ y ∈ s, x ≠ y → ∃ u v : set α, is_open u ∧ is_open v ∧
id                             └─┘  └─────┘   └─────┘  
src                                  └─┘   └─────┘    └─────┘   
typ                            └─┘  └─────┘   └─────┘  
doc                                           └─────┘     └─────┘
707    x ∈ u ∧ y ∈ v ∧ s ⊆ u ∪ v ∧ u ∩ v = ∅
id                       
src                               
typ                      
708  
709  theorem is_totally_separated_empty : is_totally_separated (∅ : set α) :=
id                                        └──────────────────┘     └─┘ 
src                                       └──────────────────┘     └─┘
typ                                       └──────────────────┘     └─┘ 
doc                                       └──────────────────┘
710  λ x, false.elim
id       └────────┘
src       └────────┘
typ      └────────┘
711  
712  theorem is_totally_separated_singleton {x} : is_totally_separated ({x} : set α) :=
id                                                └──────────────────┘      └─┘ 
src                                               └──────────────────┘       └─┘
typ                                               └──────────────────┘      └─┘ 
doc                                               └──────────────────┘
713  λ p hp q hq hpq, (hpq $ (eq_of_mem_singleton hp).symm ▸ (eq_of_mem_singleton hq).symm).elim
id      └┘  └┘ └─┘   └─┘    └─────────────────┘ └┘ └──┘    └─────────────────┘ └┘ └──┘  └──┘
src                           └─────────────────┘    └──┘    └─────────────────┘    └──┘  └──┘
typ     └┘  └┘ └─┘   └─┘    └─────────────────┘ └┘ └──┘    └─────────────────┘ └┘ └──┘  └──┘
714  
715  theorem is_totally_disconnected_of_is_totally_separated {s : set α}
id                                                                └─┘ 
src                                                               └─┘
typ                                                               └─┘ 
716    (H : is_totally_separated s) : is_totally_disconnected s :=
id          └──────────────────┘     └─────────────────────┘ 
src         └──────────────────┘      └─────────────────────┘
typ         └──────────────────┘     └─────────────────────┘ 
doc         └──────────────────┘      └─────────────────────┘
717  λ t hts ht, ⟨λ ⟨x, hxt⟩ ⟨y, hyt⟩, subtype.eq $ classical.by_contradiction $
id      └─┘ └┘       └─┘    └─┘   └────────┘   └────────────────────────┘
src                                    └────────┘   └────────────────────────┘
typ     └─┘ └┘       └─┘    └─┘   └────────┘   └────────────────────────┘
718  assume hxy : x ≠ y, let ⟨u, v, hu, hv, hxu, hyv, hsuv, huv⟩ := H x (hts hxt) y (hts hyt) hxy in
id                      └─┘      └┘  └┘  └─┘  └─┘  └──┘  └─┘         └─┘         └─┘      └─┘
src                 
typ                     └─┘      └┘  └┘  └─┘  └─┘  └──┘  └─┘         └─┘         └─┘      └─┘
719  let ⟨r, hrt, hruv⟩ := ht u v hu hv (subset.trans hts hsuv) ⟨x, hxt, hxu⟩ ⟨y, hyt, hyv⟩ in
id   └─┘         └──┘     └┘            └──────────┘ └─┘
src                                      └──────────┘
typ  └─┘         └──┘     └┘            └──────────┘ └─┘
720  ((ext_iff _ _).1 huv r).1 hruv⟩
id     └─────┘             
src    └─────┘             
typ    └─────┘             
721  
722  /-- A space is totally separated if any two points can be separated by two disjoint open sets
723  covering the whole space. -/
724  class totally_separated_space (α : Type u) [topological_space α] : Prop :=
id                                      └──┘     └───────────────┘ 
src                                              └───────────────┘
typ                                     └──┘     └───────────────┘ 
doc                                              └───────────────┘
725  (is_totally_separated_univ : is_totally_separated (univ : set α))
id                                └──────────────────┘  └──┘   └─┘ 
src                               └──────────────────┘  └──┘   └─┘
typ                               └──────────────────┘  └──┘   └─┘ 
doc                               └──────────────────┘
726  
727  @[priority 100] -- see Note [lower instance priority]
728  instance totally_separated_space.totally_disconnected_space (α : Type u) [topological_space α]
id                                                                             └───────────────┘ 
src                                                                            └───────────────┘
typ                                                                            └───────────────┘ 
doc                                                                            └───────────────┘
729    [totally_separated_space α] : totally_disconnected_space α :=
id      └─────────────────────┘     └────────────────────────┘ 
src     └─────────────────────┘      └────────────────────────┘
typ     └─────────────────────┘     └────────────────────────┘ 
doc     └─────────────────────┘      └────────────────────────┘
730  ⟨is_totally_disconnected_of_is_totally_separated $ totally_separated_space.is_totally_separated_univ α⟩
id    └─────────────────────────────────────────────┘   └───────────────────────────────────────────────┘ 
src   └─────────────────────────────────────────────┘   └───────────────────────────────────────────────┘
typ   └─────────────────────────────────────────────┘   └───────────────────────────────────────────────┘ 
731  
732  end totally_separated